| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 16:44:33 +0100 |
wenzelm |
proper identifiers for consts and types;
|
file |
diff |
annotate
|
| 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
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Wed, 15 May 2002 10:44:58 +0200 |
paulson |
better error messages for datatypes not declared Const
|
file |
diff |
annotate
|
| Mon, 19 Nov 2001 20:47:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:37:04 +0200 |
wenzelm |
use Sign.simple_read_term;
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 21:37:35 +0200 |
wenzelm |
tryres, gen_make_elim moved here;
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 11:57:09 +0100 |
paulson |
datatype package improvements
|
file |
diff |
annotate
|
| Tue, 12 Jan 1999 15:17:37 +0100 |
wenzelm |
eliminated global/local names;
|
file |
diff |
annotate
|
| Mon, 28 Dec 1998 16:59:28 +0100 |
paulson |
new inductive, datatype and primrec packages, etc.
|
file |
diff |
annotate
|
| Wed, 27 May 1998 12:23:45 +0200 |
paulson |
mk_all_imp: no longer creates goals that have beta-redexes
|
file |
diff |
annotate
|
| Fri, 10 Apr 1998 13:15:28 +0200 |
paulson |
Fixed bug in inductive sections to allow disjunctive premises;
|
file |
diff |
annotate
|
| Wed, 03 Dec 1997 10:52:17 +0100 |
paulson |
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 17:42:39 +0200 |
wenzelm |
(co) inductive / datatype package adapted to qualified names;
|
file |
diff |
annotate
|
| Thu, 28 Nov 1996 10:44:24 +0100 |
paulson |
Replaced map...~~ by ListPair.map
|
file |
diff |
annotate
|
| Tue, 26 Nov 1996 16:11:18 +0100 |
paulson |
Eta-expansion of a function definition, for value polymorphism
|
file |
diff |
annotate
|
| Wed, 08 May 1996 18:01:54 +0200 |
paulson |
moved ap_split to cartprod.ML
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 13:42:57 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Fri, 22 Dec 1995 11:09:28 +0100 |
paulson |
Improving space efficiency of inductive/datatype definitions.
|
file |
diff |
annotate
|
| Thu, 24 Nov 1994 10:57:24 +0100 |
lcp |
data_domain,Codata_domain: removed replicate; now return one
|
file |
diff |
annotate
|
| Thu, 25 Aug 1994 12:09:21 +0200 |
lcp |
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
|
file |
diff |
annotate
|
| Fri, 19 Aug 1994 16:13:53 +0200 |
wenzelm |
replaced Lexicon.scan_id by Scanner.scan_id;
|
file |
diff |
annotate
|
| Thu, 18 Aug 1994 17:41:40 +0200 |
lcp |
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
|
file |
diff |
annotate
|
| Fri, 12 Aug 1994 12:51:34 +0200 |
lcp |
installation of new inductive/datatype sections
|
file |
diff |
annotate
|
| Tue, 12 Jul 1994 14:26:04 +0200 |
clasohm |
removed flatten_typ and replaced add_consts by add_consts_i
|
file |
diff |
annotate
|
| Mon, 11 Jul 1994 13:15:05 +0200 |
clasohm |
removed flatten_term and replaced add_axioms by add_axioms_i
|
file |
diff |
annotate
|
| Fri, 01 Jul 1994 11:03:42 +0200 |
clasohm |
replaced extend_theory by new add_* functions;
|
file |
diff |
annotate
|
| Tue, 21 Jun 1994 17:20:34 +0200 |
lcp |
Addition of cardinals and order types, various tidying
|
file |
diff |
annotate
|
| Tue, 18 Jan 1994 16:37:12 +0100 |
lcp |
Updated refs to old Sign functions
|
file |
diff |
annotate
|
| Tue, 21 Dec 1993 16:38:45 +0100 |
nipkow |
added []-field to extend_theory: no type abbreviations.
|
file |
diff |
annotate
|