| 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
|
| Wed, 12 Jan 2011 15:15:51 +0100 |
wenzelm |
more FIXMEs concerning bad catch-all exception handlers;
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 15:11:56 +0100 |
wenzelm |
avoid ML structure aliases (especially single-letter abbreviations);
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 20:21:39 +0200 |
wenzelm |
do not intercept ML exceptions -- printing exception positions/text is the job of the Isar/ML toplevel;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 00:47:23 +0100 |
wenzelm |
typedef etc.: no constraints;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 14:43:04 +0100 |
wenzelm |
global typedef;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 00:36:12 +0200 |
wenzelm |
standardized basic operations on type option;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 16:58:03 +0200 |
wenzelm |
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 23:30:58 +0100 |
wenzelm |
minimal adaptions for abstract binding type;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 18:27:43 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Wed, 22 Oct 2008 14:15:44 +0200 |
haftmann |
tuned typedef interface
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 08:15:40 +0200 |
haftmann |
PureThy: dropped note_thmss_qualified, dropped _i suffix
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 17:06:14 +0200 |
wenzelm |
proper Sign operations instead of Theory aliases;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 01:25:24 +0200 |
wenzelm |
TextIO.inputLine: use present SML B library version;
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 17:07:26 +0200 |
haftmann |
slight cleanup
|
file |
diff |
annotate
|
| Thu, 06 Apr 2006 16:13:17 +0200 |
haftmann |
cleanup in typedef/datatype package
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 16:03:31 +0100 |
obua |
Added HOL-ZF to Isabelle.
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 14:59:57 +0100 |
obua |
cache improvements
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 04:17:19 +0100 |
obua |
variable counter is now also cached
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 23:57:06 +0100 |
obua |
fixed bugs, added caching
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:38 +0200 |
wenzelm |
OldGoals;
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 10:01:14 +0200 |
obua |
replay type_introduction fix
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 00:52:13 +0200 |
obua |
add debug messages
|
file |
diff |
annotate
|
| Fri, 16 Sep 2005 21:02:15 +0200 |
obua |
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 15:52:00 +0200 |
obua |
Added HOLLight support to importer.
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Sat, 17 Apr 2004 23:53:35 +0200 |
skalberg |
Minor cleanup of headers and some speedup of the HOL4 import.
|
file |
diff |
annotate
|
| Fri, 02 Apr 2004 17:37:45 +0200 |
skalberg |
Added HOL proof importer.
|
file |
diff |
annotate
|