Tue, 05 Sep 2000 10:15:23 +0200 |
paulson |
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
|
file |
diff |
annotate
|
Sun, 16 Jul 2000 20:49:33 +0200 |
wenzelm |
added Tuple.thy;
|
file |
diff |
annotate
|
Thu, 13 Jul 2000 11:41:40 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 21 Jun 2000 15:58:23 +0200 |
wenzelm |
fixed deps;
|
file |
diff |
annotate
|
Tue, 30 May 2000 16:08:38 +0200 |
wenzelm |
cleaned up;
|
file |
diff |
annotate
|
Wed, 24 May 2000 12:21:26 +0200 |
paulson |
restored NatSum.thy
|
file |
diff |
annotate
|
Tue, 23 May 2000 12:36:36 +0200 |
paulson |
theory file NatSum.thy no longer needed
|
file |
diff |
annotate
|
Fri, 05 May 2000 12:51:33 +0200 |
nipkow |
Added AVL
|
file |
diff |
annotate
|
Fri, 24 Mar 2000 17:28:03 +0100 |
wenzelm |
added HOL/ex/Multiquote.thy;
|
file |
diff |
annotate
|
Thu, 23 Mar 2000 10:22:08 +0100 |
paulson |
restored the MESON examples file HOL/ex/mesontest2.ML
|
file |
diff |
annotate
|
Wed, 08 Mar 2000 16:14:12 +0100 |
paulson |
new theory ex/Factorization
|
file |
diff |
annotate
|
Fri, 20 Aug 1999 15:41:53 +0200 |
wenzelm |
if_svc_enabled;
|
file |
diff |
annotate
|
Fri, 06 Aug 1999 17:28:45 +0200 |
paulson |
svc_enabled is now declared as a function
|
file |
diff |
annotate
|
Fri, 06 Aug 1999 11:05:20 +0200 |
paulson |
new theory ex/svc_test.thy
|
file |
diff |
annotate
|
Tue, 03 Aug 1999 13:15:54 +0200 |
paulson |
new examples file for SVC
|
file |
diff |
annotate
|
Mon, 26 Jul 1999 16:30:50 +0200 |
paulson |
HOL/ex/Tarski: new example by Florian Kammueller
|
file |
diff |
annotate
|
Thu, 11 Mar 1999 13:20:35 +0100 |
wenzelm |
removed foo_build_completed -- now handled by session management (via usedir);
|
file |
diff |
annotate
|
Mon, 16 Nov 1998 10:37:54 +0100 |
paulson |
removed the reference to mesontest2.ML, itself now deleted
|
file |
diff |
annotate
|
Fri, 23 Oct 1998 20:28:33 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 24 Aug 1998 18:17:25 +0200 |
wenzelm |
added Antiquote example;
|
file |
diff |
annotate
|
Tue, 04 Aug 1998 18:40:18 +0200 |
wenzelm |
added LocaleGroup, PiSets examples;
|
file |
diff |
annotate
|
Fri, 24 Jul 1998 17:55:57 +0200 |
wenzelm |
added ex/MonoidGroups (record example);
|
file |
diff |
annotate
|
Fri, 03 Jul 1998 17:35:39 +0200 |
wenzelm |
stepping stones: Recdef, Main;
|
file |
diff |
annotate
|
Thu, 25 Jun 1998 13:57:34 +0200 |
paulson |
Installation of target HOL-Real
|
file |
diff |
annotate
|
Mon, 20 Apr 1998 10:37:00 +0200 |
paulson |
proving fib(gcd(m,n)) = gcd(fib m, fib n)
|
file |
diff |
annotate
|
Fri, 19 Dec 1997 10:28:33 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 05 Jun 1997 13:26:09 +0200 |
paulson |
Now loads theory Recdef
|
file |
diff |
annotate
|
Mon, 26 May 1997 12:34:05 +0200 |
paulson |
Primrec: New example ported from ZF
|
file |
diff |
annotate
|
Thu, 22 May 1997 15:08:14 +0200 |
paulson |
New example: ex/Fib
|
file |
diff |
annotate
|
Tue, 20 May 1997 11:44:25 +0200 |
paulson |
Removal of ex/LexProd
|
file |
diff |
annotate
|
Wed, 07 May 1997 13:51:22 +0200 |
paulson |
Moved induction examples to directory Induct
|
file |
diff |
annotate
|
Fri, 18 Apr 1997 11:53:55 +0200 |
paulson |
Now loads theory LList indirectly: via LFilter
|
file |
diff |
annotate
|
Fri, 29 Nov 1996 15:08:06 +0100 |
nipkow |
Moved the Rings stuff from ex to Integ and showed that int::cring.
|
file |
diff |
annotate
|
Tue, 26 Nov 1996 14:26:38 +0100 |
nipkow |
Added Lagrang. Modified comment.
|
file |
diff |
annotate
|
Fri, 14 Jun 1996 12:25:19 +0200 |
paulson |
Added new Primes theory
|
file |
diff |
annotate
|
Mon, 06 May 1996 10:39:54 +0200 |
paulson |
Now mentions but does not load mesontest2.ML
|
file |
diff |
annotate
|
Thu, 04 Apr 1996 10:24:38 +0200 |
paulson |
New example Comb: Church-Rosser for combinators, ported from ZF
|
file |
diff |
annotate
|
Wed, 27 Mar 1996 18:48:50 +0100 |
paulson |
New mutilated checkerboard example
|
file |
diff |
annotate
|
Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
Tue, 21 Nov 1995 12:43:09 +0100 |
clasohm |
removed make_chart;
|
file |
diff |
annotate
|
Tue, 24 Oct 1995 14:50:24 +0100 |
clasohm |
added calls of init_html and make_chart
|
file |
diff |
annotate
|
Fri, 30 Jun 1995 11:39:20 +0200 |
lcp |
added mention of new theories BT and Perm
|
file |
diff |
annotate
|
Thu, 29 Jun 1995 12:48:48 +0200 |
clasohm |
renamed CHOL to HOL
|
file |
diff |
annotate
|
Mon, 10 Apr 1995 08:49:00 +0200 |
nipkow |
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
|
file |
diff |
annotate
|
Fri, 24 Mar 1995 12:30:35 +0100 |
clasohm |
changed syntax of tuples from <..., ...> to (..., ...)
|
file |
diff |
annotate
|
Wed, 22 Mar 1995 13:22:42 +0100 |
clasohm |
fixed bug: HOL_build_completed replaced by CHOL_build_completed
|
file |
diff |
annotate
|
Wed, 22 Mar 1995 12:42:34 +0100 |
clasohm |
converted ex with curried function application
|
file |
diff |
annotate
|