| 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
|