On Sun, Aug 5, 2012 at 12:25 PM, Rob Arthan <r...@lemma-one.com> wrote: > > On 5 Aug 2012, at 08:18, Bill Richter wrote: > >> Thanks, Ramana! I've often wanted Isabelle locales. Are you going to code >> them in HOL4? > > Locales are one of the many things that (I believe) make the Isabelle HOL > logic much more bloated than the original and best HOL logic as supported by > HOL4, HOL Light, HOL Zero and ProofPower. It might be possible to give a > similar facility as a bolt-on outside the logic.
I think everyone agrees that locales _can_ be extra-logical. I was also under the impression that they _are_ that way in Isabelle/HOL. (This is in contrast to axiomatic type classes, which are in Isabelle's logic from Pure upwards.) Anyone who knows better about locales as implemented in Isabelle, correct me if I'm wrong. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
