src/HOL/IsaMakefile
Thu, 03 Nov 2011 10:29:05 +1100 kleing moved latex generation for HOL-IMP out of distribution
Tue, 01 Nov 2011 10:05:28 +0100 bulwahn renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
Tue, 25 Oct 2011 16:37:11 +0200 bulwahn renaming Cset and List_Cset in Quotient_Examples to Quotient_Set and List_Quotient_Set to avoid a name clash of theory names with the ones in HOL-Library
Mon, 24 Oct 2011 10:45:54 +0200 nipkow latex output not needed because errors manifest themselves earlier
Sat, 22 Oct 2011 20:17:50 +0200 nipkow added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
Fri, 21 Oct 2011 08:42:11 +0200 huffman add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
Wed, 19 Oct 2011 09:11:20 +0200 bulwahn removing old code generator
Wed, 19 Oct 2011 08:37:25 +0200 bulwahn removing old code generator for inductive predicates
Wed, 19 Oct 2011 08:37:16 +0200 bulwahn removing old code generator setup in the HOL theory
Wed, 19 Oct 2011 08:37:15 +0200 bulwahn removing invocations of the evaluation method based on the old code generator
Wed, 28 Sep 2011 09:59:55 +0200 nipkow Added dependecies
Wed, 28 Sep 2011 09:55:11 +0200 nipkow Added Hoare-like Abstract Interpretation
Wed, 28 Sep 2011 08:51:55 +0200 nipkow moved IMP/AbsInt stuff into subdirectory Abs_Int_Den
Mon, 26 Sep 2011 20:39:18 +0200 wenzelm reverted 09cdc4209d25 for formal reasons: it did not say what was "broken" nor "fixed", but broke IsaMakefile dependencies;
Sun, 25 Sep 2011 09:37:33 +0200 haftmann Quotient_Set.thy is part of library
Sat, 24 Sep 2011 00:17:32 +0100 sultana fixed IsaMakefile action for HOL-TPTP.
Thu, 22 Sep 2011 18:23:38 +0200 berghofe Moved extraction part of Higman's lemma to separate theory to allow reuse in
Thu, 22 Sep 2011 16:50:23 +0200 berghofe Added documentation for HOL-SPARK
Wed, 21 Sep 2011 15:55:16 +0200 blanchet reintroduced Minipick as Nitpick example
Wed, 21 Sep 2011 07:03:16 +0200 nipkow added missing makefile dependence
Tue, 20 Sep 2011 05:47:11 +0200 nipkow New proof method "induction" that gives induction hypotheses the name IH.
Sun, 18 Sep 2011 13:39:33 +0200 wenzelm finite sequences as useful as introductory example;
Tue, 13 Sep 2011 09:28:03 +0200 bulwahn correcting theory name and dependencies
Mon, 12 Sep 2011 10:57:58 +0200 bulwahn moving connection of association lists to Mappings into a separate theory
Sat, 10 Sep 2011 10:29:24 +0200 haftmann renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
Wed, 07 Sep 2011 23:38:52 +0200 haftmann theory of saturated naturals contributed by Peter Gammie
Fri, 02 Sep 2011 19:25:44 +0200 nipkow merged
Fri, 02 Sep 2011 19:25:18 +0200 nipkow Added Abstract Interpretation theories
Fri, 02 Sep 2011 14:43:20 +0200 blanchet renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
Wed, 24 Aug 2011 15:06:13 -0700 huffman move everything related to 'norm' method into new theory file Norm_Arith.thy
Sun, 21 Aug 2011 22:13:04 +0200 krauss removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy
Thu, 18 Aug 2011 18:10:23 -0700 huffman add Multivariate_Analysis dependencies
Thu, 18 Aug 2011 13:10:24 +0200 haftmann avoid case-sensitive name for example theory
Wed, 17 Aug 2011 14:32:48 -0700 huffman IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library
Wed, 17 Aug 2011 13:14:20 +0200 wenzelm moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
Thu, 11 Aug 2011 09:41:21 +0200 krauss removed obsolete recdef-related examples
Wed, 10 Aug 2011 20:12:36 +0200 wenzelm moved old code generator to src/Tools/;
Tue, 09 Aug 2011 09:05:21 +0200 blanchet load lambda-lifting structure earlier, so it can be used in Metis
Tue, 02 Aug 2011 11:52:57 +0200 krauss moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
Tue, 02 Aug 2011 10:36:50 +0200 krauss moved recdef package to HOL/Library/Old_Recdef.thy
Mon, 01 Aug 2011 09:31:10 -0700 huffman new theory HOL/Library/Product_Lattice.thy
Tue, 26 Jul 2011 18:11:38 +0200 bulwahn more precise dependencies
Mon, 25 Jul 2011 10:43:14 +0200 bulwahn removing SML_Quickcheck
Wed, 20 Jul 2011 13:29:54 +0200 boehmes more precise dependencies
Wed, 20 Jul 2011 13:27:01 +0200 boehmes merged
Wed, 20 Jul 2011 09:23:09 +0200 boehmes removed old (unused) SMT monomorphizer
Wed, 20 Jul 2011 10:48:00 +0200 hoelzl merged
Tue, 19 Jul 2011 14:36:12 +0200 hoelzl Rename extreal => ereal
Tue, 19 Jul 2011 14:35:44 +0200 hoelzl rename Nat_Infinity (inat) to Extended_Nat (enat)
Wed, 20 Jul 2011 10:11:08 +0200 Cezary Kaliszyk HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
Wed, 20 Jul 2011 08:46:17 +0200 kleing build an image for HOL-IMP
Thu, 14 Jul 2011 22:08:11 +0200 krauss added missing dependencies;
Wed, 13 Jul 2011 22:16:19 +0200 blanchet cleanly separate TPTP related files from other examples
Wed, 13 Jul 2011 15:50:45 +0200 krauss experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package
Wed, 06 Jul 2011 17:19:34 +0100 blanchet moved ATP dependencies to HOL-Plain, where they belong
Fri, 01 Jul 2011 11:26:02 +0200 bulwahn improving actual dependencies
Mon, 27 Jun 2011 09:42:46 +0200 hoelzl move conditional expectation to its own theory file
Wed, 22 Jun 2011 13:30:28 -0700 huffman add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
Fri, 17 Jun 2011 20:38:43 +0200 kleing IMP compiler with int, added reverse soundness direction
Thu, 09 Jun 2011 08:32:15 +0200 bulwahn adapting IsaMakefile
less more (0) -1000 -300 -100 -60 tip