| Thu, 11 May 2023 10:46:52 +0200 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Tue, 26 Nov 2019 08:09:44 +0100 |
ballarin |
Remove diagnostic command 'print_dependencies'.
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 22:19:19 +0100 |
wenzelm |
isabelle update_inner_syntax_cartouches;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 21:15:52 +0100 |
wenzelm |
isabelle update -u mixfix_cartouches;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 15:31:43 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Fri, 02 Mar 2018 14:19:25 +0100 |
ballarin |
Proper rewrite morphisms in locale instances.
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 19:28:05 +0100 |
ballarin |
Experimental support for rewrite morphisms in locale instances.
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sat, 06 Jan 2018 17:34:41 +0100 |
nipkow |
tuned op
|
file |
diff |
annotate
|
| Sun, 03 Dec 2017 13:22:09 +0100 |
wenzelm |
discontinued old 'def' command;
|
file |
diff |
annotate
|
| Fri, 01 Jan 2016 10:49:00 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 18 Nov 2015 21:18:33 +0100 |
ballarin |
Refine the supression of abbreviations for morphisms that are not identities.
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 15:48:17 +0100 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:52 +0100 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:49 +0100 |
ballarin |
Qualifiers in locale expressions default to mandatory regardless of the command.
|
file |
diff |
annotate
|
| Mon, 19 Oct 2015 23:00:07 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Mon, 19 Oct 2015 20:29:29 +0200 |
wenzelm |
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2015 14:25:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 18:18:12 +0200 |
wenzelm |
evade popular keyword;
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 15:05:56 +0100 |
wenzelm |
do not test details of error messages;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 21:58:54 +0100 |
wenzelm |
enabled test in PIDE interaction;
|
file |
diff |
annotate
|
| Mon, 10 Feb 2014 17:20:11 +0100 |
wenzelm |
prefer vacuous definitional type classes over axiomatic ones;
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 22:12:47 +0200 |
ballarin |
New test case: interpretation in named contexts is not persistent.
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 22:12:47 +0200 |
ballarin |
Terminology: mixin -> rewrite morphism.
|
file |
diff |
annotate
|
| Mon, 25 Mar 2013 19:53:44 +0100 |
ballarin |
Fix issue related to mixins in roundup.
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 15:39:01 +0200 |
wenzelm |
added some ad-hoc namespace prefixes to avoid duplicate facts;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2011 12:19:54 +0200 |
ballarin |
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
|
file |
diff |
annotate
|
| Fri, 18 Feb 2011 17:03:30 +0100 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Thu, 06 Jan 2011 21:06:18 +0100 |
ballarin |
Diagnostic command to show locale dependencies.
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 13:24:04 +0100 |
wenzelm |
actually enable show_hyps option, unlike local_setup in 6da953d30f48 which merely affects the (temporary) auxiliary context;
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 18:43:16 +0100 |
ballarin |
Add mixins to locale dependencies.
|
file |
diff |
annotate
|
| Sat, 18 Dec 2010 18:43:14 +0100 |
ballarin |
Enable show_hyps, which appears to be set in batch mode but in an interactive session.
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 21:14:20 +0200 |
ballarin |
print_interps shows interpretations in proofs.
|
file |
diff |
annotate
|
| Sat, 31 Jul 2010 21:14:20 +0200 |
ballarin |
Interpretation in proofs supports mixins.
|
file |
diff |
annotate
|
| Thu, 27 May 2010 18:10:37 +0200 |
wenzelm |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Wed, 26 May 2010 21:20:18 +0200 |
ballarin |
Revise locale test theory layout.
|
file |
diff |
annotate
|