| 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
|
| Tue, 19 Sep 2006 05:54:17 +0200 |
huffman |
add Real/RealVector.thy
|
file |
diff |
annotate
|
| Thu, 14 Sep 2006 15:25:23 +0200 |
krauss |
updated makefile
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 08:34:45 +0200 |
haftmann |
added yet another code generator example
|
file |
diff |
annotate
|
| Tue, 29 Aug 2006 14:31:12 +0200 |
haftmann |
added typecopy_package and some examples
|
file |
diff |
annotate
|
| Mon, 21 Aug 2006 11:02:39 +0200 |
haftmann |
added some codegen examples/applications
|
file |
diff |
annotate
|
| Mon, 14 Aug 2006 13:46:08 +0200 |
haftmann |
added new files
|
file |
diff |
annotate
|
| Tue, 08 Aug 2006 08:19:06 +0200 |
haftmann |
added Tools/typedef_codegen.ML
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 15:03:49 +0200 |
wenzelm |
added HOL/ex/Reflection;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 14:57:26 +0200 |
ballarin |
Restructured algebra library, added ideals and quotient rings.
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 19:49:47 +0200 |
wenzelm |
added ex/Guess.thy;
|
file |
diff |
annotate
|
| Fri, 23 Jun 2006 09:55:01 +0200 |
paulson |
Introduction of Ramsey's theorem
|
file |
diff |
annotate
|
| Sun, 11 Jun 2006 00:42:22 +0200 |
dixon |
updated IsaMakefiles for new location of IsaPlanner.
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 01:51:22 +0200 |
wenzelm |
removed obsolete ML files;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 01:06:53 +0200 |
wenzelm |
removed obsolete ML files;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 00:57:14 +0200 |
wenzelm |
removed obsolete ML files;
|
file |
diff |
annotate
|
| Sun, 04 Jun 2006 10:50:41 +0200 |
mengj |
Functions of Tools/ATP/res_clasimpset.ML are now in Tools/res_atp.ML. res_clasimpset.ML is not used anymore.
|
file |
diff |
annotate
|
| Tue, 16 May 2006 13:01:22 +0200 |
wenzelm |
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
|
file |
diff |
annotate
|