| Sun, 19 Sep 2021 21:37:14 +0200 |
wenzelm |
clarified signature -- prefer antiquotations (with subtle change of exception content);
|
file |
diff |
annotate
|
| Sat, 11 Sep 2021 22:38:41 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 11 Sep 2021 22:28:01 +0200 |
wenzelm |
clarified antiquotation;
|
file |
diff |
annotate
|
| Sat, 11 Sep 2021 22:02:12 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2016 20:15:20 +0200 |
wenzelm |
eliminated unused simproc identifier;
|
file |
diff |
annotate
|
| Sat, 10 Oct 2015 22:19:06 +0200 |
wenzelm |
tuned syntax -- more symbols;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2015 11:13:54 +0100 |
wenzelm |
slightly more formal historic examples;
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 11:18:36 +0100 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 14:41:08 +0200 |
haftmann |
integrated appendix theory into main theory;
|
file |
diff |
annotate
|
| Mon, 11 Nov 2013 20:50:12 +0100 |
wenzelm |
tuned signature -- removed obsolete Addsimprocs, Delsimprocs;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Sat, 17 Sep 2011 15:08:55 +0200 |
haftmann |
dropped unused argument – avoids problem with SML/NJ
|
file |
diff |
annotate
|
| Thu, 02 Dec 2010 16:04:22 +0100 |
wenzelm |
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 10:20:37 +0100 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 10:18:05 +0100 |
wenzelm |
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 18:36:22 +0200 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 22:30:51 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Sat, 13 Feb 2010 23:24:57 +0100 |
wenzelm |
modernized structures;
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 22:06:37 +0100 |
wenzelm |
numeral syntax: clarify parse trees vs. actual terms;
|
file |
diff |
annotate
|
| Sun, 07 Feb 2010 19:31:55 +0100 |
wenzelm |
prefer explicit @{lemma} over adhoc forward reasoning;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 00:52:37 +0200 |
wenzelm |
explicitly qualify Drule.standard;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 23:12:21 +0200 |
wenzelm |
more @{theory} antiquotations;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 15:24:18 +0100 |
wenzelm |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 17:54:51 +0200 |
wenzelm |
converted ML proofs;
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 18:02:25 +0200 |
wenzelm |
OldGoals.inst;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2008 15:01:03 +0100 |
wenzelm |
tuned ML code, more antiquotations;
|
file |
diff |
annotate
|
| Mon, 11 Feb 2008 21:32:12 +0100 |
wenzelm |
removed unnecessary theory qualifiers;
|
file |
diff |
annotate
|
| Mon, 11 Feb 2008 15:40:21 +0100 |
krauss |
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
|
file |
diff |
annotate
|
| Sun, 07 Oct 2007 21:19:31 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 16:08:00 +0200 |
wenzelm |
simplified type int (eliminated IntInf.int, integer);
|
file |
diff |
annotate
|
| Thu, 31 May 2007 12:06:31 +0200 |
wenzelm |
moved Integ files to canonical place;
|
file |
diff |
annotate
|