| 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
|