src/HOL/IsaMakefile
Fri, 01 Mar 2002 16:24:43 +0100 prensani Completed annonce of HoareParallel
Tue, 26 Feb 2002 15:45:32 +0100 kleing introduces SystemClasses and BVExample
Tue, 26 Feb 2002 00:24:37 +0100 wenzelm Isar_examples/W_correct moved to W0;
Thu, 21 Feb 2002 20:08:09 +0100 wenzelm theory Option has been assimilated by Datatype;
Thu, 21 Feb 2002 14:08:09 +0100 kleing new MicroJava document
Sat, 16 Feb 2002 20:59:34 +0100 wenzelm converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
Tue, 05 Feb 2002 23:18:08 +0100 wenzelm moved SVC stuff to ex;
Mon, 28 Jan 2002 17:52:13 +0100 schirmer Bali added
Fri, 18 Jan 2002 18:35:39 +0100 wenzelm fixed document setup of HOL-Library;
Thu, 17 Jan 2002 19:37:42 +0100 nipkow Lex dependencies modified
Sun, 13 Jan 2002 21:09:17 +0100 wenzelm added HOL/Real/document/root.tex;
Sun, 13 Jan 2002 19:42:30 +0100 wenzelm Real/Complex_Numbers.thy;
Wed, 09 Jan 2002 17:48:40 +0100 wenzelm converted theory Transitive_Closure;
Tue, 08 Jan 2002 21:02:15 +0100 wenzelm HOL-Hyperreal produces an image (again);
Wed, 19 Dec 2001 00:26:39 +0100 wenzelm HOL/IMP: include session graph;
Sun, 16 Dec 2001 00:20:17 +0100 kleing MicroJava exception merge
Mon, 10 Dec 2001 15:18:34 +0100 berghofe Added new files (code generator and examples).
Sun, 09 Dec 2001 14:36:14 +0100 kleing HOL/IMP converted to Isar
Thu, 06 Dec 2001 17:15:53 +0100 wenzelm include session graph;
Thu, 06 Dec 2001 00:38:55 +0100 wenzelm renamed theory Finite to Finite_Set and converted;
Tue, 04 Dec 2001 17:59:36 +0100 wenzelm added Higher_Order_Logic.thy;
Wed, 21 Nov 2001 00:33:04 +0100 wenzelm theory Inverse_Image converted and moved to Set;
Tue, 20 Nov 2001 20:54:12 +0100 wenzelm tuned;
Fri, 16 Nov 2001 18:24:11 +0100 paulson even more theories from Jacques
Thu, 15 Nov 2001 16:12:49 +0100 paulson new theories from Jacques Fleuriot
Thu, 08 Nov 2001 17:42:43 +0100 wenzelm ex/document/root.bib;
Tue, 06 Nov 2001 23:45:34 +0100 wenzelm renamed Real/ex/Sqrt_Irrational.thy to Real/ex/Sqrt.thy;
Mon, 05 Nov 2001 13:55:48 +0100 paulson new Sqrt example
Sat, 03 Nov 2001 01:35:11 +0100 wenzelm moved String into Main;
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
less more (0) -300 -100 -60 tip