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
|
Fri, 20 Oct 2006 18:22:24 +0200 |
haftmann |
removed antisym_setup.ML
|
file |
diff |
annotate
|
Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
Fri, 13 Oct 2006 18:12:58 +0200 |
berghofe |
Added new package for inductive definitions, moved old package
|
file |
diff |
annotate
|
Fri, 06 Oct 2006 03:49:36 +0200 |
kleing |
examples for hex and bin numerals
|
file |
diff |
annotate
|
Sun, 01 Oct 2006 22:19:23 +0200 |
wenzelm |
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
|
file |
diff |
annotate
|
Sun, 01 Oct 2006 18:29:25 +0200 |
wenzelm |
moved Infinite_Set.thy to Library;
|
file |
diff |
annotate
|
Fri, 29 Sep 2006 22:47:51 +0200 |
wenzelm |
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
|
file |
diff |
annotate
|
Thu, 28 Sep 2006 23:42:32 +0200 |
wenzelm |
removed obsolete Real/document/root.tex;
|
file |
diff |
annotate
|
Thu, 28 Sep 2006 16:01:48 +0200 |
paulson |
clearout of obsolete code
|
file |
diff |
annotate
|
Tue, 19 Sep 2006 18:18:11 +0200 |
wenzelm |
moved Import/susp.ML to Pure/General;
|
file |
diff |
annotate
|
Tue, 19 Sep 2006 15:22:21 +0200 |
haftmann |
added OperationalEquality.thy
|
file |
diff |
annotate
|