src/FOL/ex/Locale_Test/Locale_Test1.thy
2014-03-10 wenzelm 2014-03-10 enabled test in PIDE interaction;
2014-02-10 wenzelm 2014-02-10 prefer vacuous definitional type classes over axiomatic ones;
2013-09-03 ballarin 2013-09-03 New test case: interpretation in named contexts is not persistent.
2013-09-03 ballarin 2013-09-03 Terminology: mixin -> rewrite morphism.
2013-03-25 ballarin 2013-03-25 Fix issue related to mixins in roundup. Previously, mixins were only applied one level down the DFS tree while they should also be applied at the level of declaration. Makes the algorithm consistent with the version presented in the upcoming JAR paper.
2012-10-10 wenzelm 2012-10-10 added some ad-hoc namespace prefixes to avoid duplicate facts;
2011-06-25 ballarin 2011-06-25 While reading equations of an interpretation, already allow syntax provided by the interpretation base.
2011-02-18 wenzelm 2011-02-18 modernized specifications;
2011-01-06 ballarin 2011-01-06 Diagnostic command to show locale dependencies.
2010-12-20 wenzelm 2010-12-20 actually enable show_hyps option, unlike local_setup in 6da953d30f48 which merely affects the (temporary) auxiliary context;
2010-12-18 ballarin 2010-12-18 Add mixins to locale dependencies.
2010-12-18 ballarin 2010-12-18 Enable show_hyps, which appears to be set in batch mode but in an interactive session.
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-07-31 ballarin 2010-07-31 print_interps shows interpretations in proofs.
2010-07-31 ballarin 2010-07-31 Interpretation in proofs supports mixins.
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-26 ballarin 2010-05-26 Revise locale test theory layout.