| Tue, 04 Jul 2000 10:54:46 +0200 |
oheimb |
disambiguated := ; added Examples (factorial)
|
file |
diff |
annotate
|
| Wed, 28 Jun 2000 10:37:08 +0200 |
paulson |
new file Provers/make_elim.ML
|
file |
diff |
annotate
|
| Fri, 23 Jun 2000 14:00:43 +0200 |
berghofe |
Added new theory Lambda/Type.
|
file |
diff |
annotate
|
| Wed, 21 Jun 2000 18:09:09 +0200 |
wenzelm |
fixed deps;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2000 12:07:07 +0200 |
paulson |
Real/simproc.ML now removed
|
file |
diff |
annotate
|
| Fri, 02 Jun 2000 12:44:04 +0200 |
oheimb |
added HOL/Prolog
|
file |
diff |
annotate
|
| Wed, 24 May 2000 18:46:38 +0200 |
paulson |
Adding SetInterval, deleting UNITY/LessThan
|
file |
diff |
annotate
|
| Wed, 24 May 2000 12:21:26 +0200 |
paulson |
restored NatSum.thy
|
file |
diff |
annotate
|
| Tue, 23 May 2000 18:24:48 +0200 |
paulson |
IntRingDefs is now redundant
|
file |
diff |
annotate
|
| Tue, 23 May 2000 12:44:03 +0200 |
paulson |
theory file NatSum.thy no longer needed
|
file |
diff |
annotate
|
| Mon, 22 May 2000 16:05:22 +0200 |
wenzelm |
new Isar version of HOL-AxClasses-Tutorial;
|
file |
diff |
annotate
|
| Mon, 22 May 2000 12:28:34 +0200 |
paulson |
new file Induct/MultisetOrder.thy
|
file |
diff |
annotate
|
| Mon, 15 May 2000 10:33:32 +0200 |
paulson |
added the dummy theory Integ/NatSimprocs.thy
|
file |
diff |
annotate
|
| Mon, 08 May 2000 20:59:30 +0200 |
wenzelm |
moved theory Sexp to Induct examples;
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:25:17 +0200 |
wenzelm |
removed Pure/section_utils.ML;
|
file |
diff |
annotate
|
| Fri, 05 May 2000 12:51:33 +0200 |
nipkow |
Added AVL
|
file |
diff |
annotate
|
| Tue, 02 May 2000 18:40:16 +0200 |
paulson |
combine_numerals replaces both fold_Suc and combine_coeff
|
file |
diff |
annotate
|
| Fri, 21 Apr 2000 11:27:28 +0200 |
paulson |
Provers/Arith/inverse_fold.ML is already obsolete
|
file |
diff |
annotate
|
| Tue, 18 Apr 2000 15:51:59 +0200 |
paulson |
new simprocs for numerals of type "nat"
|
file |
diff |
annotate
|
| Wed, 05 Apr 2000 21:08:24 +0200 |
wenzelm |
added Isar_examples/NestedDatatype.thy;
|
file |
diff |
annotate
|
| Fri, 24 Mar 2000 17:28:03 +0100 |
wenzelm |
added HOL/ex/Multiquote.thy;
|
file |
diff |
annotate
|
| Thu, 23 Mar 2000 11:27:52 +0100 |
wenzelm |
ex/Antiquote.thy made new-style theory;
|
file |
diff |
annotate
|
| Thu, 23 Mar 2000 10:22:08 +0100 |
paulson |
restored the MESON examples file HOL/ex/mesontest2.ML
|
file |
diff |
annotate
|
| Fri, 17 Mar 2000 17:12:07 +0100 |
wenzelm |
fixed dep;
|
file |
diff |
annotate
|
| Thu, 16 Mar 2000 00:35:27 +0100 |
wenzelm |
added HOL/PreLIst.thy;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2000 16:14:12 +0100 |
paulson |
new theory ex/Factorization
|
file |
diff |
annotate
|
| Sat, 04 Mar 2000 11:42:12 +0100 |
paulson |
new theories UNITY/Detects, UNITY/Reachability
|
file |
diff |
annotate
|
| Fri, 18 Feb 2000 15:37:08 +0100 |
paulson |
Rename: theory for applying a bijection over states to a UNITY program
|
file |
diff |
annotate
|
| Fri, 04 Feb 2000 21:45:57 +0100 |
wenzelm |
added MicroJava/document;
|
file |
diff |
annotate
|
| Tue, 01 Feb 2000 18:18:09 +0100 |
oheimb |
added forgotten rules to make IMPP
|
file |
diff |
annotate
|