src/HOL/IsaMakefile
2010-03-23 hoelzl 2010-03-23 Generate image for HOL-Probability
2010-03-22 bulwahn 2010-03-22 merged
2010-03-22 bulwahn 2010-03-22 removed unused Predicate_Compile_Set
2010-03-19 blanchet 2010-03-19 move the Sledgehammer Isar commands together into one file; this will make easier to add options and reorganize them later
2010-03-19 blanchet 2010-03-19 more Sledgehammer refactoring
2010-03-16 hoelzl 2010-03-16 Added product measure space
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-17 blanchet 2010-03-17 renamed "ATP_Linkup" theory to "Sledgehammer"
2010-03-17 blanchet 2010-03-17 move Sledgehammer files in a directory of their own
2010-03-13 wenzelm 2010-03-13 removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
2010-03-11 haftmann 2010-03-11 merged
2010-03-11 haftmann 2010-03-11 Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
2010-03-10 haftmann 2010-03-10 split off theory Big_Operators from theory Finite_Set
2010-03-10 huffman 2010-03-10 remove obsolete theory Nat_Int_Bij
2010-03-10 huffman 2010-03-10 new theory Library/Nat_Bijection.thy
2010-03-06 haftmann 2010-03-06 added Table.thy
2010-03-04 hoelzl 2010-03-04 Add Lebesgue integral and probability space.
2010-03-02 bulwahn 2010-03-02 adding HOL-Mutabelle to tests
2010-03-02 krauss 2010-03-02 removed obsolete helper theory
2010-02-24 haftmann 2010-02-24 renamed theory Rational to Rat
2010-02-23 hoelzl 2010-02-23 merged
2010-02-23 hoelzl 2010-02-23 Moved old Integration to examples.
2010-02-23 haftmann 2010-02-23 merged
2010-02-23 haftmann 2010-02-23 dropped session W0; c.f. MiniML in AFP
2010-02-23 haftmann 2010-02-23 merged
2010-02-22 haftmann 2010-02-22 added missing separator
2010-02-22 haftmann 2010-02-22 distributed theory Algebras to theories Groups and Lattices
2010-02-22 hoelzl 2010-02-22 Replaced Integration by Multivariate-Analysis/Real_Integration
2010-02-20 wenzelm 2010-02-20 more precise dependencies;
2010-02-19 Cezary Kaliszyk 2010-02-19 Initial version of HOL quotient package.
2010-02-16 boehmes 2010-02-16 added Cache_IO: cache for output of external tools, changed SMT solver interface to use Cache_IO
2010-02-10 wenzelm 2010-02-10 renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
2010-02-10 haftmann 2010-02-10 revert uninspired Structure_Syntax experiment
2010-02-09 blanchet 2010-02-09 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
2010-02-05 blanchet 2010-02-05 added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
2010-02-04 blanchet 2010-02-04 split "nitpick_hol.ML" into two files to make it more manageable; more refactoring to come
2010-02-08 wenzelm 2010-02-08 more precise dependencies;
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-08 haftmann 2010-02-08 merged
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures
2010-02-08 haftmann 2010-02-08 separate theory for index structures
2010-02-02 boehmes 2010-02-02 updated dependencies
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2010-01-25 bulwahn 2010-01-25 adding Mutabelle to repository
2010-01-22 bulwahn 2010-01-22 merged
2010-01-20 bulwahn 2010-01-20 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
2010-01-22 haftmann 2010-01-22 more accurate dependencies
2010-01-02 krauss 2010-01-02 absorb structures Decompose and Descent into Termination, to simplify further restructuring
2009-12-29 wenzelm 2009-12-29 explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
2009-12-18 blanchet 2009-12-18 polished Nitpick's binary integer support etc.; etc. = improve inconsistent scope correction + sort values nicely in output + handle "mod" using the characterization "x mod y = x - x div y * y" (instead of explicit code in Nitpick) + introduce KK = Kodkod as abbreviation
2009-12-11 boehmes 2009-12-11 updated dependencies
2009-12-11 boehmes 2009-12-11 depend on HOL-SMT instead of HOL (makes tactic "smt" available for proofs)
2009-12-07 haftmann 2009-12-07 split off evaluation mechanisms in separte module Code_Eval
2009-12-07 haftmann 2009-12-07 merged Crude_Executable_Set into Executable_Set
2009-12-04 haftmann 2009-12-04 merged
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-27 haftmann 2009-11-27 renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
2009-11-24 haftmann 2009-11-24 backported parts of abstract byte code verifier from AFP/Jinja
2009-12-02 haftmann 2009-12-02 added Crude_Executable_Set.thy
2009-11-20 wenzelm 2009-11-20 load ML directly into theory Code_Generator (quickcheck also requires this);