| Fri, 20 Sep 2024 23:37:00 +0200 |
wenzelm |
more inner syntax markup: minor object-logics;
|
file |
diff |
annotate
|
| Tue, 27 Sep 2022 17:46:52 +0100 |
paulson |
More syntactic cleanup. LaTeX markup working
|
file |
diff |
annotate
|
| Tue, 27 Sep 2022 16:51:35 +0100 |
paulson |
Removal of obsolete ASCII syntax
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 21:15:52 +0100 |
wenzelm |
isabelle update -u mixfix_cartouches;
|
file |
diff |
annotate
|
| Sun, 24 Jun 2018 15:57:48 +0200 |
wenzelm |
simplified ZF theory names (in contrast to 6a0801279f4c): session-qualification already achieves disjointness;
|
file |
diff |
annotate
|
| Wed, 12 Apr 2017 13:48:07 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 11:50:15 +0200 |
wenzelm |
tuned text;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2017 20:44:35 +0200 |
wenzelm |
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
|
file |
diff |
annotate
| base
|
| Tue, 04 Apr 2017 23:21:16 +0200 |
wenzelm |
allow to load this into "isabelle jedit -l HOL";
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 21:28:09 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 12 Jan 2016 00:18:43 +0100 |
wenzelm |
clarified axiomatization versus definitions;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 17:45:18 +0100 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 17:38:57 +0100 |
wenzelm |
clarified print modes;
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:23:50 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 20:26:03 +0200 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2015 14:25:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 16:39:54 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Mon, 10 Feb 2014 17:20:11 +0100 |
wenzelm |
prefer vacuous definitional type classes over axiomatic ones;
|
file |
diff |
annotate
|
| Wed, 08 Aug 2012 12:51:20 +0200 |
wenzelm |
proper axiomatization of "mem" -- do not leave it formally unspecified;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2012 10:58:43 +0200 |
wenzelm |
clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 22:22:05 +0100 |
wenzelm |
modernized axiomatization;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 17:11:49 +0000 |
paulson |
Structured proofs concerning the square of an infinite cardinal
|
file |
diff |
annotate
|
| Tue, 06 Mar 2012 15:15:49 +0000 |
paulson |
mathematical symbols instead of ASCII
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 17:13:54 +0000 |
paulson |
Removal of obsolete ML bindings
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 20:15:02 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Thu, 11 Aug 2011 11:40:25 +0200 |
wenzelm |
redundant use of misc_legacy.ML;
|
file |
diff |
annotate
|
| Fri, 18 Feb 2011 17:03:30 +0100 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 16:44:33 +0100 |
wenzelm |
proper identifiers for consts and types;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:43:54 +0100 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|