| Thu, 26 Oct 2000 14:59:38 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 25 Oct 2000 18:31:21 +0200 |
wenzelm |
"List prefixes" library theory (replaces old Lex/Prefix);
|
file |
diff |
annotate
|
| Thu, 19 Oct 2000 21:21:20 +0200 |
wenzelm |
added Tools/induct_attrib.ML;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2000 23:44:52 +0200 |
wenzelm |
removed Library/Accessible_Part.ML;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2000 23:33:04 +0200 |
wenzelm |
added HOL/Library, rearranged several files;
|
file |
diff |
annotate
|
| Fri, 13 Oct 2000 08:28:21 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 12 Oct 2000 18:38:23 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 06 Oct 2000 01:04:56 +0200 |
wenzelm |
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
|
file |
diff |
annotate
|
| Tue, 03 Oct 2000 22:34:49 +0200 |
wenzelm |
added Isar_examples/Hoare.thy Isar_examples/HoareEx.thy;
|
file |
diff |
annotate
|
| Tue, 03 Oct 2000 18:34:20 +0200 |
wenzelm |
reorganized AxClasses;
|
file |
diff |
annotate
|
| Wed, 27 Sep 2000 19:36:31 +0200 |
wenzelm |
proper Hyperreal setup;
|
file |
diff |
annotate
|
| Fri, 22 Sep 2000 13:16:24 +0200 |
kleing |
removed JVM/Store.ML, added theorem Digest in MicroJava
|
file |
diff |
annotate
|
| Thu, 21 Sep 2000 15:58:13 +0200 |
wenzelm |
renamed HOL/ex/Points to HOL/ex/Records;
|
file |
diff |
annotate
|
| Wed, 13 Sep 2000 18:45:10 +0200 |
paulson |
moved Primes, Fib, Factorization to HOL/NumberTheory
|
file |
diff |
annotate
|
| Tue, 12 Sep 2000 10:50:29 +0200 |
wenzelm |
added MicroJava/document/root.bib;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 20:48:51 +0200 |
wenzelm |
added Provers/rulify.ML;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 21:06:01 +0200 |
wenzelm |
improved meson setup;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 10:15:23 +0200 |
paulson |
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
|
file |
diff |
annotate
|
| Mon, 04 Sep 2000 10:24:55 +0200 |
paulson |
Converting HOL/ex/Primes.thy to new style, removing Primes.ML
|
file |
diff |
annotate
|
| Mon, 04 Sep 2000 09:40:28 +0200 |
nipkow |
BCV
|
file |
diff |
annotate
|
| Sat, 02 Sep 2000 22:42:04 +0200 |
wenzelm |
Lambda/document/root.tex;
|
file |
diff |
annotate
|
| Sat, 02 Sep 2000 21:56:24 +0200 |
wenzelm |
HOL/Lambda: converted into new-style theory and document;
|
file |
diff |
annotate
|
| Fri, 01 Sep 2000 00:30:25 +0200 |
wenzelm |
converted Lambda scripts;
|
file |
diff |
annotate
|
| Thu, 31 Aug 2000 01:42:23 +0200 |
wenzelm |
ported HOL/Lambda/ListBeta;
|
file |
diff |
annotate
|
| Wed, 30 Aug 2000 21:44:12 +0200 |
kleing |
MicroJava changed (all of BV -> Isar)
|
file |
diff |
annotate
|
| Tue, 29 Aug 2000 00:57:24 +0200 |
wenzelm |
Lambda/InductTermi made new-style theory;
|
file |
diff |
annotate
|
| Fri, 18 Aug 2000 17:53:49 +0200 |
wenzelm |
Main now new-style theory; added Main.ML for compatibility;
|
file |
diff |
annotate
|
| Thu, 17 Aug 2000 16:23:50 +0200 |
wenzelm |
removed Lambda/Type.ML;
|
file |
diff |
annotate
|
| Mon, 14 Aug 2000 18:08:26 +0200 |
kleing |
added MicroJava/BV/StepMono.thy,
|
file |
diff |
annotate
|
| Mon, 07 Aug 2000 14:34:26 +0200 |
kleing |
MicroJava structure changed
|
file |
diff |
annotate
|
| Thu, 03 Aug 2000 19:28:37 +0200 |
wenzelm |
tuned TLA;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2000 10:53:06 +0200 |
paulson |
new files Integ/IntPower.{thy.ML}; tidied
|
file |
diff |
annotate
|
| Mon, 31 Jul 2000 14:37:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 31 Jul 2000 12:50:33 +0200 |
nipkow |
Removed Quot
|
file |
diff |
annotate
|
| Thu, 27 Jul 2000 18:27:25 +0200 |
wenzelm |
added theory While;
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 00:06:46 +0200 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|
| Tue, 18 Jul 2000 13:16:48 +0200 |
kleing |
MicroJava structure changed
|
file |
diff |
annotate
|
| Sun, 16 Jul 2000 20:49:13 +0200 |
wenzelm |
added ex/Tuple.thy;
|
file |
diff |
annotate
|
| Fri, 14 Jul 2000 16:32:51 +0200 |
oheimb |
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
|
file |
diff |
annotate
|
| Fri, 07 Jul 2000 16:46:02 +0200 |
oheimb |
added IMP/Examples.ML dependence
|
file |
diff |
annotate
|
| Wed, 05 Jul 2000 17:52:24 +0200 |
oheimb |
disambiguated := ; added Examples (factorial)
|
file |
diff |
annotate
|
| 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
|