src/HOL/IsaMakefile
Thu, 11 Mar 2010 17:39:45 +0100 haftmann merged
Thu, 11 Mar 2010 14:39:58 +0100 haftmann Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
Wed, 10 Mar 2010 16:53:27 +0100 haftmann split off theory Big_Operators from theory Finite_Set
Wed, 10 Mar 2010 16:00:51 -0800 huffman remove obsolete theory Nat_Int_Bij
Wed, 10 Mar 2010 14:57:13 -0800 huffman new theory Library/Nat_Bijection.thy
Sat, 06 Mar 2010 15:31:30 +0100 haftmann added Table.thy
Thu, 04 Mar 2010 21:52:26 +0100 hoelzl Add Lebesgue integral and probability space.
Tue, 02 Mar 2010 22:13:32 +0100 bulwahn adding HOL-Mutabelle to tests
Tue, 02 Mar 2010 17:45:10 +0100 krauss removed obsolete helper theory
Wed, 24 Feb 2010 14:34:40 +0100 haftmann renamed theory Rational to Rat
Tue, 23 Feb 2010 17:55:00 +0100 hoelzl merged
Tue, 23 Feb 2010 17:33:03 +0100 hoelzl Moved old Integration to examples.
Tue, 23 Feb 2010 14:11:32 +0100 haftmann merged
Tue, 23 Feb 2010 10:11:31 +0100 haftmann dropped session W0; c.f. MiniML in AFP
Tue, 23 Feb 2010 08:04:07 +0100 haftmann merged
Mon, 22 Feb 2010 16:03:44 +0100 haftmann added missing separator
Mon, 22 Feb 2010 15:53:18 +0100 haftmann distributed theory Algebras to theories Groups and Lattices
Mon, 22 Feb 2010 20:41:49 +0100 hoelzl Replaced Integration by Multivariate-Analysis/Real_Integration
Sat, 20 Feb 2010 23:23:04 +0100 wenzelm more precise dependencies;
Fri, 19 Feb 2010 13:54:19 +0100 Cezary Kaliszyk Initial version of HOL quotient package.
Tue, 16 Feb 2010 15:25:36 +0100 boehmes added Cache_IO: cache for output of external tools,
Wed, 10 Feb 2010 19:37:34 +0100 wenzelm renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
Wed, 10 Feb 2010 14:12:02 +0100 haftmann revert uninspired Structure_Syntax experiment
Tue, 09 Feb 2010 17:06:05 +0100 blanchet merged (manual for "nitpick_hol.ML" and "kodkod.ML")
Fri, 05 Feb 2010 14:27:21 +0100 blanchet added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
Thu, 04 Feb 2010 16:03:15 +0100 blanchet split "nitpick_hol.ML" into two files to make it more manageable;
Mon, 08 Feb 2010 21:26:52 +0100 wenzelm more precise dependencies;
Mon, 08 Feb 2010 17:12:38 +0100 haftmann renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
Mon, 08 Feb 2010 14:08:32 +0100 haftmann merged
Mon, 08 Feb 2010 14:06:41 +0100 haftmann separate library theory for type classes combining lattices with various algebraic structures
Mon, 08 Feb 2010 10:36:02 +0100 haftmann separate theory for index structures
Tue, 02 Feb 2010 19:30:08 +0100 boehmes updated dependencies
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Mon, 25 Jan 2010 16:19:42 +0100 bulwahn adding Mutabelle to repository
Fri, 22 Jan 2010 15:26:29 +0100 bulwahn merged
Wed, 20 Jan 2010 11:56:45 +0100 bulwahn refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
Fri, 22 Jan 2010 13:38:29 +0100 haftmann more accurate dependencies
Sat, 02 Jan 2010 23:18:58 +0100 krauss absorb structures Decompose and Descent into Termination, to simplify further restructuring
Tue, 29 Dec 2009 16:20:39 +0100 wenzelm explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
Fri, 18 Dec 2009 12:00:29 +0100 blanchet polished Nitpick's binary integer support etc.;
Fri, 11 Dec 2009 15:36:05 +0100 boehmes updated dependencies
Fri, 11 Dec 2009 15:06:12 +0100 boehmes depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)
Mon, 07 Dec 2009 16:27:48 +0100 haftmann split off evaluation mechanisms in separte module Code_Eval
Mon, 07 Dec 2009 14:54:01 +0100 haftmann merged Crude_Executable_Set into Executable_Set
Fri, 04 Dec 2009 12:22:09 +0100 haftmann merged
Mon, 30 Nov 2009 11:42:49 +0100 haftmann modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
Fri, 27 Nov 2009 08:41:10 +0100 haftmann renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
Tue, 24 Nov 2009 14:37:23 +0100 haftmann backported parts of abstract byte code verifier from AFP/Jinja
Wed, 02 Dec 2009 17:53:34 +0100 haftmann added Crude_Executable_Set.thy
Fri, 20 Nov 2009 15:33:10 +0100 wenzelm load ML directly into theory Code_Generator (quickcheck also requires this);
Wed, 18 Nov 2009 09:34:53 +0100 boehmes added arithmetic example using div and mod
Tue, 17 Nov 2009 18:52:30 +0100 hoelzl Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
Sat, 14 Nov 2009 19:56:18 +0100 wenzelm moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
Thu, 12 Nov 2009 20:38:57 +0100 bulwahn added a tabled implementation of the reflexive transitive closure
Tue, 10 Nov 2009 13:54:00 +0100 blanchet merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
Thu, 05 Nov 2009 11:58:36 +0100 blanchet merged
Thu, 29 Oct 2009 23:08:51 +0100 blanchet merged
Thu, 29 Oct 2009 15:26:00 +0100 blanchet merged
Thu, 29 Oct 2009 12:09:32 +0100 blanchet merged
Wed, 28 Oct 2009 18:09:30 +0100 blanchet merged my Auto Nitpick change with Lukas's Predicate Compiler changes
less more (0) -1000 -300 -100 -60 tip