src/FOL/ex/LocaleTest.thy
2008-08-06 ballarin 2008-08-06 Interpretation command (theory/proof context) no longer simplifies goal.
2008-08-04 ballarin 2008-08-04 Updated locale tests.
2008-07-25 haftmann 2008-07-25 dropped locale (open)
2008-07-16 ballarin 2008-07-16 Removed uses of context element includes.
2008-04-14 ballarin 2008-04-14 Changed naming scheme for theorems generated by interpretations.
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-03-05 wenzelm 2008-03-05 explicit referencing of background facts;
2007-11-05 ballarin 2007-11-05 Tests enforce proper export behaviour.
2007-10-01 ballarin 2007-10-01 unfold_locales workaround
2007-08-31 wenzelm 2007-08-31 do not touch quick_and_dirty;
2007-07-23 ballarin 2007-07-23 interpretation: equations are propositions not pairs of terms;
2007-05-11 wenzelm 2007-05-11 tuned proofs;
2007-04-20 ballarin 2007-04-20 Interpretation equations applied to attributes
2007-04-13 ballarin 2007-04-13 Experimental code for the interpretation of definitions.
2006-09-04 ballarin 2006-09-04 More locale test code.
2006-07-07 ballarin 2006-07-07 Modified comment.
2006-07-04 ballarin 2006-07-04 Method intro_locales replaced by intro_locales and unfold_locales.
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2006-06-06 ballarin 2006-06-06 Improved parameter management of locales.
2005-09-16 ballarin 2005-09-16 tuned
2005-09-02 ballarin 2005-09-02 print_locale omits facts by default
2005-08-24 ballarin 2005-08-24 Printing of interpretations: option to show witness theorems;
2005-08-17 ballarin 2005-08-17 Improved generation of witnesses in interpretation.
2005-08-08 ballarin 2005-08-08 Release of interpretation in locale.
2005-08-02 ballarin 2005-08-02 First version of interpretation in locales. Not yet fully functional.
2005-07-07 ballarin 2005-07-07 Preparations for interpretation of locales in locales.
2005-06-30 ballarin 2005-06-30 Proper treatment of beta-redexes in witness theorems.
2005-06-08 ballarin 2005-06-08 Fixed "axiom" generation for mixed locales with and without predicates.
2005-06-01 ballarin 2005-06-01 Locales: new element constrains, parameter renaming with syntax, experimental command instantiate withdrawn.
2005-05-27 ballarin 2005-05-27 Locale expressions: rename with optional mixfix syntax.
2005-04-25 ballarin 2005-04-25 Subsumption of locale interpretations.
2005-04-18 ballarin 2005-04-18 Interpretation supports statically scoped attributes; documentation.
2005-04-11 ballarin 2005-04-11 First release of interpretation commands.
2005-03-24 ballarin 2005-03-24 Further work on interpretation commands. New command `interpret' for interpretation in proof contexts.
2005-03-10 ballarin 2005-03-10 Registrations of global locale interpretations: improved, better naming.
2005-03-09 ballarin 2005-03-09 First version of global registration command.