| Sun, 10 Jun 2001 08:03:35 +0200 |
paulson |
new GroupTheory example, e.g. the Sylow theorem (preliminary version)
|
file |
diff |
annotate
|
| Sat, 09 Jun 2001 08:41:25 +0200 |
paulson |
moved Primes.thy from NumberTheory to Library
|
file |
diff |
annotate
|
| Fri, 08 Jun 2001 08:50:08 +0200 |
nipkow |
Removed BCV
|
file |
diff |
annotate
|
| Thu, 31 May 2001 20:53:49 +0200 |
wenzelm |
added HOL-CTL;
|
file |
diff |
annotate
|
| Thu, 31 May 2001 16:52:54 +0200 |
oheimb |
added Library/Nat_Infinity.thy and Library/Continuity.thy
|
file |
diff |
annotate
|
| Tue, 08 May 2001 15:56:57 +0200 |
paulson |
conversion of Auth/TLS to Isar script
|
file |
diff |
annotate
|
| Tue, 24 Apr 2001 12:19:01 +0200 |
paulson |
(rough) conversion of Auth/Recur to Isar format
|
file |
diff |
annotate
|
| Thu, 12 Apr 2001 12:45:05 +0200 |
paulson |
converted many HOL/Auth theories to Isar scripts
|
file |
diff |
annotate
|
| Wed, 28 Mar 2001 13:39:50 +0200 |
nipkow |
MicroJava/BV dependencies incomplete
|
file |
diff |
annotate
|
| Fri, 23 Mar 2001 10:10:53 +0100 |
nipkow |
added one point simprocs for bounded quantifiers
|
file |
diff |
annotate
|
| Mon, 05 Mar 2001 15:25:11 +0100 |
paulson |
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
|
file |
diff |
annotate
|
| Fri, 02 Mar 2001 13:26:55 +0100 |
paulson |
conversion of Message.thy to Isar format
|
file |
diff |
annotate
|
| Thu, 15 Feb 2001 16:00:35 +0100 |
oheimb |
Ord.thy/.ML converted to Isar
|
file |
diff |
annotate
|
| Tue, 13 Feb 2001 15:46:03 +0100 |
paulson |
partial conversion to Isar script style in HOL/Auth removes some .ML files
|
file |
diff |
annotate
|
| Fri, 09 Feb 2001 16:22:30 +0100 |
kleing |
removed MicroJava/Digest.thy
|
file |
diff |
annotate
|
| Sun, 04 Feb 2001 19:31:13 +0100 |
wenzelm |
HOL-NumberTheory: converted to new-style format and proper document setup;
|
file |
diff |
annotate
|
| Sat, 03 Feb 2001 17:40:16 +0100 |
wenzelm |
Induct: converted some theories to new-style format;
|
file |
diff |
annotate
|
| Thu, 01 Feb 2001 20:53:13 +0100 |
oheimb |
converted to Isar, simplifying recursion on class hierarchy
|
file |
diff |
annotate
|
| Thu, 01 Feb 2001 20:51:13 +0100 |
wenzelm |
converted to new-style theories;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2001 16:46:19 +0100 |
nipkow |
fixed set comprehension print translation
|
file |
diff |
annotate
|
| Fri, 26 Jan 2001 00:19:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 26 Jan 2001 00:15:36 +0100 |
wenzelm |
Transitive_Closure turned into new-style theory;
|
file |
diff |
annotate
|
| Tue, 23 Jan 2001 18:05:53 +0100 |
wenzelm |
added HOL-Unix example;
|
file |
diff |
annotate
|
| Sat, 20 Jan 2001 00:32:56 +0100 |
wenzelm |
added Library/Ring_and_Field_Example.thy;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2001 23:53:07 +0100 |
wenzelm |
added HOL/Library/Nested_Environment.thy;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2001 19:21:21 +0100 |
kleing |
removed obsolete MicroJava/JVM/Store.thy
|
file |
diff |
annotate
|
| Tue, 16 Jan 2001 00:25:25 +0100 |
wenzelm |
removed ex/StringEx.ML;
|
file |
diff |
annotate
|
| Fri, 12 Jan 2001 11:06:50 +0100 |
wenzelm |
added Induct/Sigma_Algebra.thy;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2001 21:40:49 +0100 |
wenzelm |
removed MicroJava/BV/Convert.thy;
|
file |
diff |
annotate
|
| Fri, 05 Jan 2001 10:19:32 +0100 |
paulson |
new UNITY examples by Sidi Ehmety
|
file |
diff |
annotate
|
| Wed, 03 Jan 2001 21:23:13 +0100 |
wenzelm |
TFL: renamed .sml to .ML;
|
file |
diff |
annotate
|
| Mon, 01 Jan 2001 11:51:20 +0100 |
paulson |
put in some missing Hyperreal files
|
file |
diff |
annotate
|
| Sat, 30 Dec 2000 22:03:47 +0100 |
paulson |
separation of HOL-Hyperreal from HOL-Real
|
file |
diff |
annotate
|
| Sat, 23 Dec 2000 22:50:19 +0100 |
wenzelm |
Tools/string_syntax.ML;
|
file |
diff |
annotate
|
| Thu, 21 Dec 2000 19:19:18 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 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
|