| Sat, 03 Mar 2012 23:54:44 +0100 |
haftmann |
generalized user-visible text
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 21:00:04 +0100 |
haftmann |
explicit locations for import_theory and setup_theory, for better user interface conformance
|
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
|
| 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
|
| Wed, 12 Jan 2011 15:15:51 +0100 |
wenzelm |
more FIXMEs concerning bad catch-all exception handlers;
|
file |
diff |
annotate
|
| Sat, 13 Nov 2010 19:55:45 +0100 |
wenzelm |
total Symbol.source;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 16:32:11 +0200 |
wenzelm |
eliminated unnecessary ref;
|
file |
diff |
annotate
|
| Fri, 28 May 2010 18:15:22 +0200 |
wenzelm |
made SML/NJ quite happy;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 15:11:25 +0200 |
wenzelm |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
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
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2008 21:27:48 +0200 |
wenzelm |
Symbol.source/OuterLex.source: more explicit do_recover argument;
|
file |
diff |
annotate
|
| Thu, 07 Aug 2008 19:21:37 +0200 |
wenzelm |
Position.start;
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 17:38:32 +0200 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 16:50:04 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 17:06:14 +0200 |
wenzelm |
proper Sign operations instead of Theory aliases;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 13:28:37 +0200 |
wenzelm |
Syntax.parse/check/read;
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:25:19 +0200 |
wenzelm |
removed redundant OuterLex.make_lexicon;
|
file |
diff |
annotate
|
| Mon, 09 Jul 2007 23:12:44 +0200 |
wenzelm |
adapted OuterLex/T.source;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:35:52 +0200 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 00:11:03 +0200 |
wenzelm |
removed obsolete sign_of/sign_of_thm;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 23:57:06 +0100 |
obua |
fixed bugs, added caching
|
file |
diff |
annotate
|
| Mon, 26 Sep 2005 02:27:14 +0200 |
obua |
fixed disambiguation problem
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:21:06 +0200 |
wenzelm |
global quick_and_dirty;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 13:42:26 +0200 |
wenzelm |
OuterKeyword;
|
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
|
| Mon, 19 Apr 2004 10:57:26 +0200 |
skalberg |
Forgot a couple of checks for the quick_and_dirty flag the other day.
|
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
|
| Sun, 04 Apr 2004 15:34:14 +0200 |
skalberg |
Added a number of explicit type casts and delayed evaluations (all seemingly
|
file |
diff |
annotate
|
| Fri, 02 Apr 2004 17:37:45 +0200 |
skalberg |
Added HOL proof importer.
|
file |
diff |
annotate
|