src/HOL/IsaMakefile
Fri, 02 Nov 2001 22:01:58 +0100 wenzelm theory Calculation move to Set;
Sat, 20 Oct 2001 20:19:47 +0200 wenzelm document graphs for several sessions;
Fri, 19 Oct 2001 22:00:08 +0200 wenzelm got rid of Provers/split_paired_all.ML;
Sun, 14 Oct 2001 22:08:29 +0200 wenzelm moved rulify to ObjectLogic;
Sun, 14 Oct 2001 20:02:11 +0200 wenzelm removed Ord.thy (now part of HOL.thy).
Thu, 04 Oct 2001 15:41:43 +0200 wenzelm $(SRC)/Provers/induct_method.ML replaces Tools/induct_method.ML;
Wed, 03 Oct 2001 21:03:05 +0200 wenzelm Tools/induct_attrib.ML now part of Pure;
Mon, 01 Oct 2001 11:56:40 +0200 wenzelm added Ordinals example;
Thu, 27 Sep 2001 22:28:16 +0200 wenzelm eliminated theories "equalities" and "mono" (made part of "Typedef",
Thu, 27 Sep 2001 18:45:40 +0200 wenzelm updated;
Thu, 27 Sep 2001 15:42:30 +0200 wenzelm ex/Hilbert_Classical.thy ex/document/root.tex;
Sat, 01 Sep 2001 00:20:06 +0200 wenzelm HOL-Real-Hyperreal made a plain session (no longer an image);
Fri, 31 Aug 2001 16:27:43 +0200 berghofe Added new files for code generator.
Wed, 25 Jul 2001 13:13:01 +0200 paulson partial restructuring to reduce dependence on Axiom of Choice
Mon, 23 Jul 2001 17:46:40 +0200 paulson new GroupTheory examples; PiSets moved to GroupTheory, while LocaleGroup deleted
Tue, 03 Jul 2001 22:11:09 +0200 wenzelm Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential
Tue, 03 Jul 2001 15:28:24 +0200 paulson Locale-based group theory proofs
Sat, 16 Jun 2001 20:06:42 +0200 oheimb added NanoJava
Sun, 10 Jun 2001 08:03:35 +0200 paulson new GroupTheory example, e.g. the Sylow theorem (preliminary version)
Sat, 09 Jun 2001 08:41:25 +0200 paulson moved Primes.thy from NumberTheory to Library
Fri, 08 Jun 2001 08:50:08 +0200 nipkow Removed BCV
Thu, 31 May 2001 20:53:49 +0200 wenzelm added HOL-CTL;
Thu, 31 May 2001 16:52:54 +0200 oheimb added Library/Nat_Infinity.thy and Library/Continuity.thy
Tue, 08 May 2001 15:56:57 +0200 paulson conversion of Auth/TLS to Isar script
Tue, 24 Apr 2001 12:19:01 +0200 paulson (rough) conversion of Auth/Recur to Isar format
Thu, 12 Apr 2001 12:45:05 +0200 paulson converted many HOL/Auth theories to Isar scripts
Wed, 28 Mar 2001 13:39:50 +0200 nipkow MicroJava/BV dependencies incomplete
Fri, 23 Mar 2001 10:10:53 +0100 nipkow added one point simprocs for bounded quantifiers
Mon, 05 Mar 2001 15:25:11 +0100 paulson reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
Fri, 02 Mar 2001 13:26:55 +0100 paulson conversion of Message.thy to Isar format
Thu, 15 Feb 2001 16:00:35 +0100 oheimb Ord.thy/.ML converted to Isar
Tue, 13 Feb 2001 15:46:03 +0100 paulson partial conversion to Isar script style in HOL/Auth removes some .ML files
Fri, 09 Feb 2001 16:22:30 +0100 kleing removed MicroJava/Digest.thy
Sun, 04 Feb 2001 19:31:13 +0100 wenzelm HOL-NumberTheory: converted to new-style format and proper document setup;
Sat, 03 Feb 2001 17:40:16 +0100 wenzelm Induct: converted some theories to new-style format;
Thu, 01 Feb 2001 20:53:13 +0100 oheimb converted to Isar, simplifying recursion on class hierarchy
Thu, 01 Feb 2001 20:51:13 +0100 wenzelm converted to new-style theories;
Sun, 28 Jan 2001 16:46:19 +0100 nipkow fixed set comprehension print translation
Fri, 26 Jan 2001 00:19:50 +0100 wenzelm tuned;
Fri, 26 Jan 2001 00:15:36 +0100 wenzelm Transitive_Closure turned into new-style theory;
Tue, 23 Jan 2001 18:05:53 +0100 wenzelm added HOL-Unix example;
Sat, 20 Jan 2001 00:32:56 +0100 wenzelm added Library/Ring_and_Field_Example.thy;
Fri, 19 Jan 2001 23:53:07 +0100 wenzelm added HOL/Library/Nested_Environment.thy;
Tue, 16 Jan 2001 19:21:21 +0100 kleing removed obsolete MicroJava/JVM/Store.thy
Tue, 16 Jan 2001 00:25:25 +0100 wenzelm removed ex/StringEx.ML;
Fri, 12 Jan 2001 11:06:50 +0100 wenzelm added Induct/Sigma_Algebra.thy;
Sun, 07 Jan 2001 21:40:49 +0100 wenzelm removed MicroJava/BV/Convert.thy;
Fri, 05 Jan 2001 10:19:32 +0100 paulson new UNITY examples by Sidi Ehmety
Wed, 03 Jan 2001 21:23:13 +0100 wenzelm TFL: renamed .sml to .ML;
Mon, 01 Jan 2001 11:51:20 +0100 paulson put in some missing Hyperreal files
Sat, 30 Dec 2000 22:03:47 +0100 paulson separation of HOL-Hyperreal from HOL-Real
Sat, 23 Dec 2000 22:50:19 +0100 wenzelm Tools/string_syntax.ML;
Thu, 21 Dec 2000 19:19:18 +0100 nipkow *** empty log message ***
Tue, 19 Dec 2000 15:19:12 +0100 paulson new file extract_common_term.ML for the cancel-factor simprocs
Sat, 16 Dec 2000 21:41:51 +0100 wenzelm tuned HOL/Real/HahnBanach;
Wed, 06 Dec 2000 20:05:58 +0100 wenzelm added Library/Rational_Numbers.thy;
Fri, 01 Dec 2000 19:53:29 +0100 nipkow Linear arithmetic now copes with mixed nat/int formulae.
Wed, 29 Nov 2000 10:19:32 +0100 paulson new simproc file cancel_numeral_factor.ML
Fri, 17 Nov 2000 18:47:15 +0100 wenzelm Library/Ring_and_Field.thy;
Fri, 10 Nov 2000 19:08:30 +0100 wenzelm proper theory context for mesontest2;
less more (0) -100 -60 tip