Hi Brian, I am not totally happy with changes like:
http://isabelle.in.tum.de/reports/Isabelle/rev/4657b4c11138#l1.7 The proof text itself is shorter than before, but in less trivial examples it produces head ache to instantiate foundational theorems of locale with OF. Indeed, huge parts of Finite_Set.thy once were written in that style. The disadvantage there was that when you had to instantiate over a hierarchy of locales, you would find yourselves writing ... OF [... OF [...]] cascades. From this I have drawn the conclusion that it is better to leave module system (locale + interpretation) and propositional system (_ ==> _ + _ [OF ...]) on their own, even if both are embedded into the same calculus. That particular situation is simple enough not to ask for a revert of the changesets, though. Cheers, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
