src/FOL/ex/Locale_Test/Locale_Test1.thy
17 months ago wenzelm 2017-12-03 discontinued old 'def' command;
2016-01-01 wenzelm 2016-01-01 isabelle update_cartouches -c -t;
2015-11-18 ballarin 2015-11-18 Refine the supression of abbreviations for morphisms that are not identities.
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-11-04 ballarin 2015-11-04 Keyword 'rewrites' identifies rewrite morphisms.
2015-11-04 ballarin 2015-11-04 Qualifiers in locale expressions default to mandatory regardless of the command.
2015-10-19 wenzelm 2015-10-19 more symbols; tunes whitespace;
2015-10-19 wenzelm 2015-10-19 more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2015-04-01 wenzelm 2015-04-01 evade popular keyword;
2014-03-13 wenzelm 2014-03-13 do not test details of error messages;
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.