| 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
|
| Fri, 06 Aug 1999 17:27:51 +0200 |
paulson |
new theory UNITY/Lift_prog
|
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:08:18 +0200 |
paulson |
new examples file for SVC
|
file |
diff |
annotate
|
| Mon, 02 Aug 1999 11:24:01 +0200 |
paulson |
new files for the SVC link-up
|
file |
diff |
annotate
|
| Wed, 28 Jul 1999 19:14:33 +0200 |
wenzelm |
HOL-Real target now builds an actual image;
|
file |
diff |
annotate
|
| Mon, 26 Jul 1999 16:30:50 +0200 |
paulson |
HOL/ex/Tarski: new example by Florian Kammueller
|
file |
diff |
annotate
|
| Mon, 19 Jul 1999 15:27:34 +0200 |
paulson |
NatBin: binary arithmetic for the naturals
|
file |
diff |
annotate
|
| Thu, 08 Jul 1999 13:35:33 +0200 |
paulson |
new files IntDiv.{thy,ML}
|
file |
diff |
annotate
|
| Tue, 06 Jul 1999 21:08:30 +0200 |
wenzelm |
added Numeral.thy, Tools/numeral_syntax.ML;
|
file |
diff |
annotate
|
| Thu, 01 Jul 1999 21:28:49 +0200 |
wenzelm |
Isar_examples/KnasterTarski.thy;
|
file |
diff |
annotate
|
| Fri, 11 Jun 1999 10:33:43 +0200 |
paulson |
new UNITY files
|
file |
diff |
annotate
|
| Fri, 04 Jun 1999 19:57:31 +0200 |
wenzelm |
Calculation.thy: Setup transitivity rules for calculational proofs.
|
file |
diff |
annotate
|
| Fri, 04 Jun 1999 16:17:10 +0200 |
wenzelm |
added Isar_examples/Group.thy;
|
file |
diff |
annotate
|
| Wed, 26 May 1999 22:45:59 +0200 |
wenzelm |
ex/Points Isar'ized;
|
file |
diff |
annotate
|
| Wed, 26 May 1999 10:15:03 +0200 |
paulson |
new theories Follows and ListOrder
|
file |
diff |
annotate
|
| Wed, 28 Apr 1999 13:36:31 +0200 |
paulson |
eliminated theory UNITY/Traces
|
file |
diff |
annotate
|
| Tue, 27 Apr 1999 15:10:36 +0200 |
wenzelm |
added Isar_examples/NatSum.thy;
|
file |
diff |
annotate
|
| Tue, 27 Apr 1999 10:45:20 +0200 |
wenzelm |
added Isar_examples/Cantor.ML;
|
file |
diff |
annotate
|
| Fri, 23 Apr 1999 12:20:22 +0200 |
paulson |
Addition of Auth/KerberosIV; renaming of rules.new.sml to rules.sml
|
file |
diff |
annotate
|
| Thu, 22 Apr 1999 12:47:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 22 Apr 1999 12:40:11 +0200 |
mueller |
deleted some old examples in Modelcheck;
|
file |
diff |
annotate
|
| Fri, 16 Apr 1999 17:46:02 +0200 |
wenzelm |
added Isar_examples;
|
file |
diff |
annotate
|
| Fri, 16 Apr 1999 14:49:34 +0200 |
wenzelm |
added Tools/induct_method.ML;
|
file |
diff |
annotate
|
| Wed, 14 Apr 1999 19:07:04 +0200 |
wenzelm |
Tools/inductive_package.ML;
|
file |
diff |
annotate
|
| Thu, 18 Mar 1999 11:19:03 +0100 |
paulson |
added new theory Yahalom_Bad
|
file |
diff |
annotate
|
| Wed, 03 Mar 1999 11:26:36 +0100 |
paulson |
added UNITY/Extend
|
file |
diff |
annotate
|
| Mon, 08 Feb 1999 13:02:42 +0100 |
wenzelm |
updated TLA;
|
file |
diff |
annotate
|
| Fri, 05 Feb 1999 21:12:18 +0100 |
wenzelm |
Hyperreal made part of Real;
|
file |
diff |
annotate
|
| Mon, 04 Jan 1999 15:07:47 +0100 |
nipkow |
Version 1.0 of linear nat arithmetic.
|
file |
diff |
annotate
|
| Fri, 27 Nov 1998 17:00:30 +0100 |
nipkow |
At last: linear arithmetic for nat!
|
file |
diff |
annotate
|
| Fri, 27 Nov 1998 13:13:22 +0100 |
paulson |
added Real/Hyperreal
|
file |
diff |
annotate
|
| Tue, 17 Nov 1998 10:29:28 +0100 |
paulson |
new theory UNITY/PPROD
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 16:11:01 +0200 |
narasche |
ex/Points added
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 12:59:03 +0200 |
berghofe |
Directory Induct: Added new theory ABexp, removed obsolete
|
file |
diff |
annotate
|
| Wed, 21 Oct 1998 16:34:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 20 Oct 1998 16:39:14 +0200 |
wenzelm |
split_paired_all.ML;
|
file |
diff |
annotate
|
| Tue, 13 Oct 1998 10:32:59 +0200 |
paulson |
Addition of HOL/UNITY/Client
|
file |
diff |
annotate
|
| Fri, 09 Oct 1998 11:15:39 +0200 |
nipkow |
added Induct/Multiset*
|
file |
diff |
annotate
|
| Wed, 07 Oct 1998 10:30:47 +0200 |
paulson |
new files UNITY/Comp.{thy,ML}
|
file |
diff |
annotate
|
| Tue, 06 Oct 1998 14:39:53 +0200 |
nipkow |
Merges FoldSet into Finite
|
file |
diff |
annotate
|
| Fri, 02 Oct 1998 10:42:37 +0200 |
paulson |
new files Provers/Arith/abel_cancel.ML and Real/simproc.ML
|
file |
diff |
annotate
|
| Fri, 25 Sep 1998 14:04:22 +0200 |
paulson |
Renaming of Integ/Integ.* to Integ/Int.*
|
file |
diff |
annotate
|
| Fri, 18 Sep 1998 15:08:46 +0200 |
paulson |
new files in Integ
|
file |
diff |
annotate
|
| Mon, 07 Sep 1998 10:43:31 +0200 |
paulson |
New UNITY theory, the N-S protocol
|
file |
diff |
annotate
|
| Tue, 01 Sep 1998 15:04:59 +0200 |
paulson |
new theory Induct/FoldSet
|
file |
diff |
annotate
|