> Anyway, I've asked myself the same question above, when some HOL person > will start to implement a version of "sections" or "locales". My estimate > is that when starting today, it would take approx. 5 years to make this > become real. Our very first version of Isabelle locales can be seen here > (14 years ago): > http://isabelle.in.tum.de/repos/isabelle/file/5313f781efe0/src/Pure/locale.ML > > > Makarius
My opinion is that Peter Homeier's HOL-Omega is the right setting to properly implement something locale-like, since it provides quantification over type variables in the logic. In plain old HOL the implementation of locales as essentially assumptions on goals is too limiting for polymorphism. Konrad. ------------------------------------------------------------------------------ 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