| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 11:57:52 +0100 |
haftmann |
prefer proof context over background theory
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 18:57:02 +0200 |
haftmann |
spelling
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 15:30:19 +0200 |
wenzelm |
more standard module name Axclass (according to file name);
|
file |
diff |
annotate
|
| Mon, 16 Jul 2012 21:20:56 +0200 |
wenzelm |
more direct Sorts.has_instance;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 20:47:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 15:00:49 +0100 |
wenzelm |
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 14:57:09 +0200 |
wenzelm |
simplified check/uncheck interfaces: result comparison is hardwired by default;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 17:14:48 +0100 |
wenzelm |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 18:24:44 +0100 |
haftmann |
avoid slightly odd Conv.tap_thy
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 09:47:12 +0100 |
haftmann |
simplified evaluation function names
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:33:21 +0100 |
haftmann |
keep type variable arguments of datatype constructors in bookkeeping
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 18:43:23 +0200 |
haftmann |
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 15:25:32 +0200 |
haftmann |
full palette of dynamic/static value(_strict/exn)
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 15:10:21 +0200 |
haftmann |
Factored out ML into separate file
|
file |
diff |
annotate
|