| Fri, 25 May 2007 05:18:56 +0200 |
urbanc |
took out Class.thy from the compiling process until memory problems are solved
|
file |
diff |
annotate
|
| Tue, 22 May 2007 05:07:48 +0200 |
huffman |
remove obsolete CSeries.thy
|
file |
diff |
annotate
|
| Fri, 18 May 2007 09:16:57 +0200 |
haftmann |
dropped word_setup.ML
|
file |
diff |
annotate
|
| Thu, 17 May 2007 23:03:47 +0200 |
krauss |
updated
|
file |
diff |
annotate
|
| Tue, 15 May 2007 18:28:02 +0200 |
chaieb |
A verified theory for rational numbers representation and simple calculations;
|
file |
diff |
annotate
|
| Mon, 14 May 2007 12:52:56 +0200 |
haftmann |
reorganized float arithmetic
|
file |
diff |
annotate
|
| Sun, 13 May 2007 18:15:21 +0200 |
haftmann |
added modules rat.ML and int.ML
|
file |
diff |
annotate
|
| Wed, 09 May 2007 19:37:22 +0200 |
wenzelm |
removed Complex/ComplexBin.thy;
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:49:24 +0200 |
haftmann |
dropped HOL.ML
|
file |
diff |
annotate
|
| Fri, 27 Apr 2007 14:21:23 +0200 |
urbanc |
alternative and much simpler proof for Church-Rosser of Beta-Reduction
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 16:39:31 +0200 |
wenzelm |
removed legacy ML files;
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:32:59 +0200 |
haftmann |
moved code generation pretty integers and characters to separate theories
|
file |
diff |
annotate
|
| Tue, 24 Apr 2007 15:19:33 +0200 |
berghofe |
Added datatype_case.ML and nominal_fresh_fun.ML.
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 10:00:04 +0200 |
ballarin |
New file for locale regression tests.
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 00:07:52 +0200 |
huffman |
moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy
|
file |
diff |
annotate
|
| Thu, 12 Apr 2007 03:37:30 +0200 |
huffman |
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
|
file |
diff |
annotate
|
| Wed, 11 Apr 2007 04:13:06 +0200 |
huffman |
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
|
file |
diff |
annotate
|
| Tue, 27 Mar 2007 12:28:42 +0200 |
haftmann |
cleaned up HOL/ex/Code*.thy
|
file |
diff |
annotate
|
| Mon, 26 Mar 2007 14:53:00 +0200 |
haftmann |
cleaned up Library( and ex/
|
file |
diff |
annotate
|
| Fri, 23 Mar 2007 09:40:47 +0100 |
haftmann |
removed outdated example
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 15:52:39 +0100 |
haftmann |
dropped OrderedGroup.ML
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 21:33:31 +0100 |
haftmann |
dropped LOrder.thy
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 17:17:36 +0100 |
urbanc |
adjusted for the example file SOS.thy
|
file |
diff |
annotate
|
| Wed, 28 Feb 2007 16:35:00 +0100 |
krauss |
more cleanup
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 21:34:16 +0100 |
krauss |
Added formalization of size-change principle (experimental).
|
file |
diff |
annotate
|
| Fri, 16 Feb 2007 09:04:23 +0100 |
krauss |
updated Makefile
|
file |
diff |
annotate
|
| Tue, 13 Feb 2007 18:19:25 +0100 |
berghofe |
Added new file Nominal/nominal_inductive.ML
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:26:04 +0100 |
berghofe |
Added Predicate theory.
|
file |
diff |
annotate
|
| Tue, 06 Feb 2007 00:53:15 +0100 |
urbanc |
corrected typo introduced by me
|
file |
diff |
annotate
|
| Tue, 06 Feb 2007 00:41:54 +0100 |
urbanc |
moved the infrastructure from the nominal_tags file to nominal_thmdecls
|
file |
diff |
annotate
|
| Mon, 22 Jan 2007 18:17:04 +0100 |
krauss |
Included ex/Fundefs.thy in HOL-ex session
|
file |
diff |
annotate
|
| Mon, 22 Jan 2007 17:29:43 +0100 |
krauss |
* Preliminary implementation of tail recursion
|
file |
diff |
annotate
|
| Sat, 20 Jan 2007 14:27:45 +0100 |
wenzelm |
added HOL/ex/Binary.thy;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:07 +0100 |
wenzelm |
HOL-Lambda: usedir -m no_brackets;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2007 14:11:25 +0100 |
urbanc |
fixed typo introduced by me
|
file |
diff |
annotate
|
| Tue, 16 Jan 2007 13:59:08 +0100 |
urbanc |
formalisation of Crary's chapter on logical relations
|
file |
diff |
annotate
|
| Tue, 16 Jan 2007 08:06:55 +0100 |
haftmann |
refined and added example for ExecutableRat
|
file |
diff |
annotate
|
| Wed, 03 Jan 2007 10:59:06 +0100 |
paulson |
first version of structured proof reconstruction
|
file |
diff |
annotate
|
| Wed, 27 Dec 2006 19:09:56 +0100 |
haftmann |
added code generator test theory
|
file |
diff |
annotate
|
| Sat, 16 Dec 2006 20:27:56 +0100 |
huffman |
removed Hyperreal/HyperArith.thy and Hyperreal/HyperPow.thy
|
file |
diff |
annotate
|
| Thu, 14 Dec 2006 22:19:39 +0100 |
huffman |
remove Hyperreal/fuf.ML
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 00:03:42 +0100 |
huffman |
Hyperreal/FrechetDeriv.thy
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 19:37:25 +0100 |
wenzelm |
added Tools/string_syntax.ML;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 01:12:36 +0100 |
wenzelm |
removed legacy ML bindings;
|
file |
diff |
annotate
|
| Mon, 04 Dec 2006 00:05:47 +0100 |
wenzelm |
converted legacy ML script;
|
file |
diff |
annotate
|
| Sat, 02 Dec 2006 02:52:02 +0100 |
wenzelm |
TLA: converted legacy ML scripts;
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 12:11:20 +0100 |
berghofe |
Added nominal_primrec.ML
|
file |
diff |
annotate
|
| Mon, 20 Nov 2006 21:23:12 +0100 |
wenzelm |
HOL-Prolog: converted legacy ML scripts;
|
file |
diff |
annotate
|
| Sun, 19 Nov 2006 23:48:55 +0100 |
wenzelm |
HOL-Algebra: converted legacy ML scripts;
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 11:41:40 +0100 |
krauss |
added lexicographic_order.ML to makefile
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 23:11:13 +0100 |
wenzelm |
moved theories Parity, GCD, Binomial to Library;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 21:45:15 +0100 |
wenzelm |
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 19:48:34 +0100 |
haftmann |
renamed Lattice_Locales to Lattices
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 13:48:33 +0100 |
wenzelm |
removed NatArith.thy, Main.ML;
|
file |
diff |
annotate
|
| Mon, 06 Nov 2006 16:28:33 +0100 |
haftmann |
added state monad to HOL library
|
file |
diff |
annotate
|
| Sat, 04 Nov 2006 00:11:11 +0100 |
huffman |
new Deriv.thy contains stuff from Lim.thy
|
file |
diff |
annotate
|
| Fri, 03 Nov 2006 14:22:37 +0100 |
haftmann |
simplified reasoning tools setup
|
file |
diff |
annotate
|
| Wed, 01 Nov 2006 19:03:30 +0100 |
urbanc |
changed to not compile Iteration and Recursion, but Lam_Funs instead
|
file |
diff |
annotate
|
| Thu, 26 Oct 2006 10:48:35 +0200 |
paulson |
Conversion to clause form now tolerates Boolean variables without looping.
|
file |
diff |
annotate
|
| Mon, 23 Oct 2006 00:47:25 +0200 |
berghofe |
Added Compile and Height examples to Nominal directory.
|
file |
diff |
annotate
|