src/HOL/IsaMakefile
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);
2009-11-18 boehmes 2009-11-18 added arithmetic example using div and mod
2009-11-17 hoelzl 2009-11-17 Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
2009-11-14 wenzelm 2009-11-14 moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
2009-11-12 bulwahn 2009-11-12 added a tabled implementation of the reflexive transitive closure
2009-11-10 blanchet 2009-11-10 merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
2009-11-05 blanchet 2009-11-05 merged
2009-10-29 blanchet 2009-10-29 merged
2009-10-29 blanchet 2009-10-29 merged
2009-10-29 blanchet 2009-10-29 merged
2009-10-28 blanchet 2009-10-28 merged my Auto Nitpick change with Lukas's Predicate Compiler changes
2009-10-28 blanchet 2009-10-28 introduced Auto Nitpick in addition to Auto Quickcheck; this required generalizing the theorem hook used by Quickcheck, following a suggestion by Florian
2009-11-09 paulson 2009-11-09 New theory Probability/Borel.thy, and some associated lemmas
2009-11-06 krauss 2009-11-06 renamed method induct_scheme to induction_schema
2009-11-06 krauss 2009-11-06 removed session SizeChange: outdated, only half-functional, alternatives exist (cf. size_change method)
2009-11-05 wenzelm 2009-11-05 more accurate cleanup;
2009-11-05 wenzelm 2009-11-05 merged
2009-11-05 wenzelm 2009-11-05 more accurate dependencies;
2009-11-05 boehmes 2009-11-05 merged
2009-11-05 boehmes 2009-11-05 handle let expressions inside terms by unfolding (instead of raising an exception), added examples to test this feature
2009-11-05 boehmes 2009-11-05 shorter names for variables and verification conditions, auto-fix variables occurring in a verification condition
2009-11-05 wenzelm 2009-11-05 more accurate dependencies; tuned;
2009-11-04 krauss 2009-11-04 added Tree23 to IsaMakefile
2009-11-03 boehmes 2009-11-03 added HOL-Boogie
2009-10-30 haftmann 2009-10-30 moved Commutative_Ring into session Decision_Procs
2009-10-30 krauss 2009-10-30 absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
2009-10-29 wenzelm 2009-10-29 merged
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-29 wenzelm 2009-10-29 separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;
2009-10-29 haftmann 2009-10-29 merged
2009-10-28 haftmann 2009-10-28 moved theory Divides after theory Nat_Numeral; tuned some proof texts
2009-10-28 wenzelm 2009-10-28 tuned;
2009-10-28 paulson 2009-10-28 merged
2009-10-28 paulson 2009-10-28 New theory Probability, which contains a development of measure theory
2009-10-27 paulson 2009-10-27 merged
2009-10-27 paulson 2009-10-27 New theory SupInf of the supremum and infimum operators for sets of reals.
2009-10-27 bulwahn 2009-10-27 merged
2009-10-27 bulwahn 2009-10-27 adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
2009-10-27 bulwahn 2009-10-27 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
2009-10-27 boehmes 2009-10-27 removed unused file smt_builtin.ML, made negative pattern polymorphic (similar to positve pattern)
2009-10-26 wenzelm 2009-10-26 recovered sort indentation for "sort position", as documented in the file; more precise dependencies -- HOL-Multivariate_Analysis produces an image; tuned;
2009-10-26 blanchet 2009-10-26 merged
2009-10-26 blanchet 2009-10-26 merged
2009-10-26 blanchet 2009-10-26 merged
2009-10-23 blanchet 2009-10-23 continuation of Nitpick's integration into Isabelle; added examples, and integrated non-Main theories better.
2009-10-22 blanchet 2009-10-22 added Nitpick's theory and ML files to Isabelle/HOL; the examples and the documentation are on their way.