src/HOL/IsaMakefile
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.
2009-10-26 berghofe 2009-10-26 merged
2009-10-26 berghofe 2009-10-26 Added Pattern.thy to Nominal/Examples.
2009-10-26 wenzelm 2009-10-26 more precise dependencies, notably for HOL-Multivariate_Analysis;
2009-10-26 haftmann 2009-10-26 merged
2009-10-23 himmelma 2009-10-23 distinguished session for multivariate analysis
2009-10-23 krauss 2009-10-23 renamed auto_term.ML -> relation.ML
2009-10-23 krauss 2009-10-23 function package: more standard names for structures and files
2009-10-23 krauss 2009-10-23 renamed FundefDatatype -> Function_Fun
2009-10-23 haftmann 2009-10-23 merged
2009-10-23 haftmann 2009-10-23 turned off old quickcheck
2009-10-23 krauss 2009-10-23 pat_completeness gets its own file
2009-10-20 wenzelm 2009-10-20 modernized session SET_Protocol;
2009-10-20 wenzelm 2009-10-20 modernized session Metis_Examples;
2009-10-20 wenzelm 2009-10-20 modernized session Isar_Examples;
2009-10-20 wenzelm 2009-10-20 more accurate dependencies for HOL-SMT, which is a session with image; misc cleanup;
2009-10-20 boehmes 2009-10-20 added proof reconstructon for Z3, added certificates for simpler re-checking of proofs (no need to invoke external solvers), added examples and certificates for all examples, removed Unsynchronized.ref (in smt_normalize.ML)
2009-10-01 wenzelm 2009-10-01 more precise dependencies;
2009-09-28 wenzelm 2009-09-28 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
2009-09-24 bulwahn 2009-09-24 merged; adopted to changes from Code_Evaluation in the predicate compiler
2009-09-23 bulwahn 2009-09-23 moved predicate compiler to Tools
2009-09-23 bulwahn 2009-09-23 handling of definitions
2009-09-23 haftmann 2009-09-23 Code_Eval(uation)
2009-09-21 haftmann 2009-09-21 added session theory for Bali and Nominal_Examples
2009-09-21 haftmann 2009-09-21 added session entry point theories
2009-09-21 haftmann 2009-09-21 entry point theory for examples; reactivated half-dead example
2009-09-21 haftmann 2009-09-21 theory entry point for session Hoare_Parallel (now also with proper underscore)
2009-09-18 boehmes 2009-09-18 added new method "smt": an oracle-based connection to external SMT solvers