| Tue, 19 Dec 2000 15:19:12 +0100 |
paulson |
new file extract_common_term.ML for the cancel-factor simprocs
|
file |
diff |
annotate
|
| Sat, 16 Dec 2000 21:41:51 +0100 |
wenzelm |
tuned HOL/Real/HahnBanach;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2000 20:05:58 +0100 |
wenzelm |
added Library/Rational_Numbers.thy;
|
file |
diff |
annotate
|
| Fri, 01 Dec 2000 19:53:29 +0100 |
nipkow |
Linear arithmetic now copes with mixed nat/int formulae.
|
file |
diff |
annotate
|
| Wed, 29 Nov 2000 10:19:32 +0100 |
paulson |
new simproc file cancel_numeral_factor.ML
|
file |
diff |
annotate
|
| Fri, 17 Nov 2000 18:47:15 +0100 |
wenzelm |
Library/Ring_and_Field.thy;
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 19:08:30 +0100 |
wenzelm |
proper theory context for mesontest2;
|
file |
diff |
annotate
|
| Mon, 30 Oct 2000 18:24:20 +0100 |
wenzelm |
added ex/PER.thy;
|
file |
diff |
annotate
|
| 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
|