| Sun, 04 Mar 2012 00:15:08 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 04 Mar 2012 00:03:04 +0100 |
haftmann |
avoid internal hol4 name references in generic importer code
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 23:49:54 +0100 |
haftmann |
generalized attribute name
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 23:43:21 +0100 |
haftmann |
one unified Importer theory
|
file |
diff |
annotate
|
| Fri, 17 Feb 2012 11:24:39 +0100 |
wenzelm |
retain default of Syntax.ambiguity, according to 2bd54d4b5f3d (despite earlier versions);
|
file |
diff |
annotate
|
| Thu, 16 Feb 2012 22:18:28 +0100 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2012 11:55:06 +0100 |
wenzelm |
handle specific exception, not arbitrary ones (including Interrupt);
|
file |
diff |
annotate
|
| Fri, 13 Jan 2012 11:50:28 +0100 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
| Thu, 24 Nov 2011 20:45:34 +0100 |
wenzelm |
simplified -- empty_ss already contains minimal mksimps;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Wed, 20 Jul 2011 10:11:08 +0200 |
Cezary Kaliszyk |
HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 23:48:28 +0200 |
krauss |
killed use of PolyML.makestring
|
file |
diff |
annotate
|
| Wed, 13 Jul 2011 00:23:24 +0900 |
Cezary Kaliszyk |
HOL/Import for HOLLight revival: Proper theory headers, update generation scripts to SVN version of HOL Light, add some constant maps and compatibility theorems
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 23:12:02 +0200 |
wenzelm |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file |
diff |
annotate
|