| Wed, 17 Dec 2003 16:23:52 +0100 |
paulson |
converted Hyperreal/HyperDef to Isar script
|
file |
diff |
annotate
|
| Tue, 16 Dec 2003 15:38:09 +0100 |
paulson |
converted Hyperreal/HyperOrd to new-style theory
|
file |
diff |
annotate
|
| Wed, 10 Dec 2003 16:47:50 +0100 |
paulson |
combining Real/{RealArith0,real_arith}.ML
|
file |
diff |
annotate
|
| Wed, 10 Dec 2003 15:59:34 +0100 |
paulson |
Moving some theorems from Real/RealArith0.ML
|
file |
diff |
annotate
|
| Thu, 04 Dec 2003 16:16:36 +0100 |
paulson |
further simplifications of the integer development; converting more .ML files
|
file |
diff |
annotate
|
| Thu, 04 Dec 2003 10:29:17 +0100 |
paulson |
Tidying of the integer development; towards removing the
|
file |
diff |
annotate
|
| Fri, 28 Nov 2003 12:09:37 +0100 |
paulson |
conversion of some Real theories to Isar scripts
|
file |
diff |
annotate
|
| Thu, 27 Nov 2003 10:47:55 +0100 |
paulson |
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
|
file |
diff |
annotate
|
| Tue, 25 Nov 2003 10:37:03 +0100 |
paulson |
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
|
file |
diff |
annotate
|
| Mon, 24 Nov 2003 15:33:07 +0100 |
paulson |
conversion of integers to use Ring_and_Field;
|
file |
diff |
annotate
|
| Fri, 21 Nov 2003 11:15:40 +0100 |
paulson |
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
|
file |
diff |
annotate
|
| Thu, 20 Nov 2003 10:42:00 +0100 |
paulson |
conversion of Integ/Int_lemmas.ML to Isar script
|
file |
diff |
annotate
|
| Tue, 18 Nov 2003 11:01:52 +0100 |
paulson |
conversion of ML to Isar scripts
|
file |
diff |
annotate
|
| Wed, 22 Oct 2003 10:52:36 +0200 |
paulson |
InductiveInvariant_examples illustrates advanced recursive function definitions
|
file |
diff |
annotate
|
| Wed, 08 Oct 2003 15:57:41 +0200 |
paulson |
Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
|
file |
diff |
annotate
|
| Tue, 23 Sep 2003 15:40:27 +0200 |
paulson |
new session HOL-SET-Protocol
|
file |
diff |
annotate
|
| Thu, 04 Sep 2003 11:15:53 +0200 |
paulson |
conversion of HOL/Auth/KerberosIV to new-style theory
|
file |
diff |
annotate
|
| Fri, 15 Aug 2003 13:07:01 +0200 |
paulson |
A document for UNITY
|
file |
diff |
annotate
|
| Tue, 12 Aug 2003 13:35:03 +0200 |
paulson |
ZhouGollmann: new example (fair non-repudiation protocol)
|
file |
diff |
annotate
|
| Thu, 24 Jul 2003 18:23:17 +0200 |
paulson |
new theory Library/NatPair
|
file |
diff |
annotate
|
| Thu, 17 Jul 2003 15:23:20 +0200 |
skalberg |
Added package for definition by specification.
|
file |
diff |
annotate
|
| Thu, 03 Jul 2003 18:07:50 +0200 |
paulson |
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts
|
file |
diff |
annotate
|
| Thu, 03 Jul 2003 12:56:48 +0200 |
paulson |
converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)
|
file |
diff |
annotate
|
| Thu, 03 Jul 2003 10:37:25 +0200 |
paulson |
Conversion of UNITY/Comp/Priority.thy to a linear Isar script
|
file |
diff |
annotate
|
| Thu, 26 Jun 2003 18:20:00 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 24 Jun 2003 10:42:34 +0200 |
berghofe |
Added new theories StrongNorm and WeakNorm to Lambda example.
|
file |
diff |
annotate
|
| Mon, 26 May 2003 11:42:41 +0200 |
kleing |
set HOL_PROOF_OBJECTS in settings, not makefile (makes override in user settings possible)
|
file |
diff |
annotate
|
| Sat, 24 May 2003 19:52:53 +0200 |
kleing |
fixed
|
file |
diff |
annotate
|
| Fri, 23 May 2003 17:19:53 +0200 |
kleing |
make it possible to switch off proof objects for HOL image
|
file |
diff |
annotate
|
| Wed, 14 May 2003 20:36:29 +0200 |
schirmer |
Added Bali to test
|
file |
diff |
annotate
|