Sun, 12 Sep 2010 19:04:02 +0200 |
wenzelm |
eliminated aliases of Type.constraint;
|
file |
diff |
annotate
|
Wed, 18 Aug 2010 12:19:27 +0200 |
haftmann |
deglobalization
|
file |
diff |
annotate
|
Thu, 27 May 2010 17:41:27 +0200 |
wenzelm |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
Mon, 15 Feb 2010 17:17:51 +0100 |
wenzelm |
discontinued unnamed infix syntax;
|
file |
diff |
annotate
|
Sun, 07 Feb 2010 19:33:34 +0100 |
wenzelm |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
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
|
Sat, 17 Oct 2009 00:52:37 +0200 |
wenzelm |
explicitly qualify Drule.standard;
|
file |
diff |
annotate
|
Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 22:48:24 +0200 |
wenzelm |
modernized Balanced_Tree;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
Sat, 07 Mar 2009 22:17:25 +0100 |
wenzelm |
more uniform handling of binding in packages;
|
file |
diff |
annotate
|
Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
Wed, 18 Jun 2008 18:55:10 +0200 |
wenzelm |
eliminated old Sign.read_term/Thm.read_cterm etc.;
|
file |
diff |
annotate
|
Mon, 16 Jun 2008 22:13:39 +0200 |
wenzelm |
pervasive RuleInsts;
|
file |
diff |
annotate
|
Mon, 16 Jun 2008 17:54:43 +0200 |
wenzelm |
RuleInsts.read_instantiate;
|
file |
diff |
annotate
|
Wed, 11 Jun 2008 18:02:00 +0200 |
wenzelm |
Drule.read_instantiate;
|
file |
diff |
annotate
|
Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
Sat, 01 Mar 2008 14:10:15 +0100 |
wenzelm |
misc cleanup of embedded ML code;
|
file |
diff |
annotate
|
Mon, 11 Feb 2008 21:32:12 +0100 |
wenzelm |
removed unnecessary theory qualifiers;
|
file |
diff |
annotate
|
Mon, 11 Feb 2008 15:40:21 +0100 |
krauss |
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
|
file |
diff |
annotate
|
Sun, 07 Oct 2007 21:19:31 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
Wed, 03 Oct 2007 22:33:17 +0200 |
wenzelm |
avoid unnamed infixes;
|
file |
diff |
annotate
|
Tue, 19 Jun 2007 23:15:38 +0200 |
wenzelm |
BalancedTree;
|
file |
diff |
annotate
|
Thu, 31 May 2007 14:34:07 +0200 |
wenzelm |
removed obsolete IFOL.thy/FOL.thy values;
|
file |
diff |
annotate
|
Tue, 03 Apr 2007 19:24:11 +0200 |
wenzelm |
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
|
file |
diff |
annotate
|
Sun, 26 Nov 2006 23:43:53 +0100 |
wenzelm |
converted legacy ML scripts;
|
file |
diff |
annotate
|
Wed, 16 Nov 2005 17:45:22 +0100 |
wenzelm |
Term.betapply;
|
file |
diff |
annotate
|
Tue, 25 Oct 2005 18:18:59 +0200 |
wenzelm |
traceIt: plain term;
|
file |
diff |
annotate
|
Fri, 15 Jul 2005 15:44:22 +0200 |
wenzelm |
tuned fold on terms and lists;
|
file |
diff |
annotate
|