| Wed, 24 May 2000 12:21:26 +0200 |
paulson |
restored NatSum.thy
|
file |
diff |
annotate
|
| Tue, 23 May 2000 18:24:48 +0200 |
paulson |
IntRingDefs is now redundant
|
file |
diff |
annotate
|
| Tue, 23 May 2000 12:44:03 +0200 |
paulson |
theory file NatSum.thy no longer needed
|
file |
diff |
annotate
|
| Mon, 22 May 2000 16:05:22 +0200 |
wenzelm |
new Isar version of HOL-AxClasses-Tutorial;
|
file |
diff |
annotate
|
| Mon, 22 May 2000 12:28:34 +0200 |
paulson |
new file Induct/MultisetOrder.thy
|
file |
diff |
annotate
|
| Mon, 15 May 2000 10:33:32 +0200 |
paulson |
added the dummy theory Integ/NatSimprocs.thy
|
file |
diff |
annotate
|
| Mon, 08 May 2000 20:59:30 +0200 |
wenzelm |
moved theory Sexp to Induct examples;
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:25:17 +0200 |
wenzelm |
removed Pure/section_utils.ML;
|
file |
diff |
annotate
|
| Fri, 05 May 2000 12:51:33 +0200 |
nipkow |
Added AVL
|
file |
diff |
annotate
|
| Tue, 02 May 2000 18:40:16 +0200 |
paulson |
combine_numerals replaces both fold_Suc and combine_coeff
|
file |
diff |
annotate
|
| Fri, 21 Apr 2000 11:27:28 +0200 |
paulson |
Provers/Arith/inverse_fold.ML is already obsolete
|
file |
diff |
annotate
|
| Tue, 18 Apr 2000 15:51:59 +0200 |
paulson |
new simprocs for numerals of type "nat"
|
file |
diff |
annotate
|
| Wed, 05 Apr 2000 21:08:24 +0200 |
wenzelm |
added Isar_examples/NestedDatatype.thy;
|
file |
diff |
annotate
|
| Fri, 24 Mar 2000 17:28:03 +0100 |
wenzelm |
added HOL/ex/Multiquote.thy;
|
file |
diff |
annotate
|
| Thu, 23 Mar 2000 11:27:52 +0100 |
wenzelm |
ex/Antiquote.thy made new-style theory;
|
file |
diff |
annotate
|
| Thu, 23 Mar 2000 10:22:08 +0100 |
paulson |
restored the MESON examples file HOL/ex/mesontest2.ML
|
file |
diff |
annotate
|
| Fri, 17 Mar 2000 17:12:07 +0100 |
wenzelm |
fixed dep;
|
file |
diff |
annotate
|
| Thu, 16 Mar 2000 00:35:27 +0100 |
wenzelm |
added HOL/PreLIst.thy;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2000 16:14:12 +0100 |
paulson |
new theory ex/Factorization
|
file |
diff |
annotate
|
| Sat, 04 Mar 2000 11:42:12 +0100 |
paulson |
new theories UNITY/Detects, UNITY/Reachability
|
file |
diff |
annotate
|
| Fri, 18 Feb 2000 15:37:08 +0100 |
paulson |
Rename: theory for applying a bijection over states to a UNITY program
|
file |
diff |
annotate
|
| Fri, 04 Feb 2000 21:45:57 +0100 |
wenzelm |
added MicroJava/document;
|
file |
diff |
annotate
|
| Tue, 01 Feb 2000 18:18:09 +0100 |
oheimb |
added forgotten rules to make IMPP
|
file |
diff |
annotate
|
| Mon, 31 Jan 2000 18:30:35 +0100 |
oheimb |
added IMPP to HOL
|
file |
diff |
annotate
|
| Thu, 20 Jan 2000 17:57:59 +0100 |
wenzelm |
removed Isar_examples/Minimal;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2000 16:06:43 +0100 |
nipkow |
Forgot to "call" MicroJava in makefile.
|
file |
diff |
annotate
|
| Tue, 07 Dec 1999 12:12:54 +0100 |
wenzelm |
added Isar_examples/Fibonacci.thy;
|
file |
diff |
annotate
|
| Tue, 30 Nov 1999 16:51:41 +0100 |
paulson |
new theory UNITY/ELT
|
file |
diff |
annotate
|
| Mon, 29 Nov 1999 11:21:44 +0100 |
wenzelm |
Isar_examples/Minimal.thy;
|
file |
diff |
annotate
|
| Thu, 25 Nov 1999 12:30:57 +0100 |
nipkow |
del Method.ML
|
file |
diff |
annotate
|
| Wed, 17 Nov 1999 15:03:23 +0100 |
wenzelm |
added Isar_examples/Puzzle.thy;
|
file |
diff |
annotate
|
| Thu, 11 Nov 1999 12:24:48 +0100 |
nipkow |
Added MicroJava
|
file |
diff |
annotate
|
| Thu, 11 Nov 1999 11:29:11 +0100 |
wenzelm |
clean target;
|
file |
diff |
annotate
|
| Fri, 05 Nov 1999 12:45:37 +0100 |
paulson |
Algebra and Polynomial theories, by Clemens Ballarin
|
file |
diff |
annotate
|
| Sat, 30 Oct 1999 20:39:01 +0200 |
wenzelm |
fixed deps;
|
file |
diff |
annotate
|
| Thu, 28 Oct 1999 19:53:24 +0200 |
wenzelm |
fixed deps;
|
file |
diff |
annotate
|
| Mon, 25 Oct 1999 19:24:31 +0200 |
wenzelm |
added Real/HahnBanach/document/root.bib;
|
file |
diff |
annotate
|
| Fri, 22 Oct 1999 20:14:31 +0200 |
wenzelm |
HahnBanach update by Gertrud Bauer;
|
file |
diff |
annotate
|
| Fri, 08 Oct 1999 15:08:47 +0200 |
wenzelm |
include document;
|
file |
diff |
annotate
|
| Wed, 06 Oct 1999 18:50:40 +0200 |
wenzelm |
Isar_examples/W_correct;
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 21:43:05 +0200 |
wenzelm |
removed TFL/sys.sml;
|
file |
diff |
annotate
|
| Tue, 28 Sep 1999 22:17:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 28 Sep 1999 16:37:04 +0200 |
nipkow |
added BCV.
|
file |
diff |
annotate
|
| Tue, 28 Sep 1999 15:30:52 +0200 |
paulson |
new UNITY theory: Project
|
file |
diff |
annotate
|
| Wed, 22 Sep 1999 21:04:34 +0200 |
wenzelm |
proper theory setup for Real/ex/BinEx;
|
file |
diff |
annotate
|
| Fri, 10 Sep 1999 17:28:51 +0200 |
wenzelm |
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
|
file |
diff |
annotate
|
| Wed, 08 Sep 1999 15:37:31 +0200 |
paulson |
new example HOL/UNITY/TimerArray
|
file |
diff |
annotate
|
| Thu, 02 Sep 1999 15:25:19 +0200 |
wenzelm |
renamed NatSum to Summation;
|
file |
diff |
annotate
|
| Wed, 01 Sep 1999 21:45:48 +0200 |
wenzelm |
Isar_examples/MultisetOrder.thy;
|
file |
diff |
annotate
|
| Tue, 31 Aug 1999 15:58:38 +0200 |
paulson |
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
|
file |
diff |
annotate
|
| Mon, 30 Aug 1999 20:29:28 +0200 |
wenzelm |
clean: include HOL-Real-ex;
|
file |
diff |
annotate
|
| Mon, 30 Aug 1999 17:18:20 +0200 |
paulson |
make it actually RUN the real examples
|
file |
diff |
annotate
|
| Mon, 30 Aug 1999 15:25:16 +0200 |
paulson |
new directory HOL/Real/ex of real examples
|
file |
diff |
annotate
|
| Sun, 29 Aug 1999 17:52:44 +0200 |
wenzelm |
added Isar_examples/MutilatedCheckerboard.thy;
|
file |
diff |
annotate
|
| Wed, 25 Aug 1999 20:49:02 +0200 |
wenzelm |
proper bootstrap of HOL theory and packages;
|
file |
diff |
annotate
|
| Tue, 24 Aug 1999 11:54:13 +0200 |
wenzelm |
Real/Real.thy main entry point;
|
file |
diff |
annotate
|
| Fri, 20 Aug 1999 15:43:25 +0200 |
wenzelm |
eliminated HOL-AxClasses target;
|
file |
diff |
annotate
|
| Fri, 20 Aug 1999 11:54:32 +0200 |
paulson |
new theories RealBin, RealInt, RealPow
|
file |
diff |
annotate
|
| Tue, 17 Aug 1999 17:33:47 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 16 Aug 1999 18:41:06 +0200 |
paulson |
new theory Real/Hyperreal/HyperDef and file fuf.ML
|
file |
diff |
annotate
|