> 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

Reply via email to