2011-03-23 blanchet 2011-03-23 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" default to "e" rather than "vampire" since E is part of the Isabelle bundle
2011-03-22 blanchet 2011-03-22 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
2011-03-22 blanchet 2011-03-22 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers
2011-03-21 krauss 2011-03-21 more precise dependencies
2011-03-21 krauss 2011-03-21 small test case for main mirabelle functionality, which easily breaks without noticing
2011-03-14 hoelzl 2011-03-14 reworked Probability theory: measures are not type restricted to positive extended reals
2011-03-14 hoelzl 2011-03-14 split Extended_Reals into parts for Library and Multivariate_Analysis
2011-03-14 hoelzl 2011-03-14 add Extended_Reals from AFP/Lower_Semicontinuous
2011-03-13 wenzelm 2011-03-13 eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
2011-03-11 bulwahn 2011-03-11 adaptions in generators using the common functions
2011-03-11 bulwahn 2011-03-11 adding file quickcheck_common to carry common functions of all quickcheck generators
2011-03-11 bulwahn 2011-03-11 correcting dependencies in IsaMakefile
2011-03-11 bulwahn 2011-03-11 moving exhaustive_generators.ML to Quickcheck directory
2011-03-11 bulwahn 2011-03-11 correcting dependencies after renaming
2011-03-11 bulwahn 2011-03-11 adding lazysmallcheck example theory to HOL-ex session
2011-03-11 bulwahn 2011-03-11 adding Lazysmallcheck prototype to HOL-Library
2011-03-03 wenzelm 2011-03-03 eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;
2011-02-26 nipkow 2011-02-26 Corrected HOLCF/FOCUS dependency
2011-02-26 nipkow 2011-02-26 corrected HOLCF dependency on Nat_Infinity
2011-02-23 noschinl 2011-02-23 setup case_product attribute in HOL and FOL
2011-01-19 hoelzl 2011-01-19 merged
2011-01-18 hoelzl 2011-01-18 Gauge measure removed
2011-01-15 haftmann 2011-01-15 experimental variant of interpretation with simultaneous definitions, plus example
2011-01-15 berghofe 2011-01-15 Also added SPARK to test and clean targets.
2011-01-15 berghofe 2011-01-15 Added HOL-SPARK and removed old_primrec.ML
2011-01-11 haftmann 2011-01-11 "enriched_type" replaces less specific "type_lifting"
2011-01-10 krauss 2011-01-10 removed obsolete make target (now in doc-src, cf. 28b487cd9e15)
2011-01-08 wenzelm 2011-01-08 renamed Sum_Of_Squares to Sum_of_Squares;
2011-01-07 bulwahn 2011-01-07 adding example theory for list comprehension to set comprehension simproc
2011-01-07 bulwahn 2011-01-07 adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
2011-01-03 boehmes 2011-01-03 re-implemented support for datatypes (including records and typedefs); added test cases for datatypes, records and typedefs
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-29 wenzelm 2010-12-29 made SML/NJ happy; more accurate dependencies;
2010-12-21 blanchet 2010-12-21 renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name); use it in "Mirabelle.thy"
2010-12-19 huffman 2010-12-19 reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
2010-12-19 huffman 2010-12-19 renamed Bifinite.thy to Representable.thy
2010-12-17 huffman 2010-12-17 renamed CompactBasis.thy to Compact_Basis.thy
2010-12-15 blanchet 2010-12-15 example tuning
2010-12-11 huffman 2010-12-11 add HOLCF library theories with cpo/predomain instances for HOL types
2010-12-08 blanchet 2010-12-08 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
2010-12-07 boehmes 2010-12-07 merged
2010-12-07 boehmes 2010-12-07 moved smt_word.ML into the directory of the Word library
2010-12-07 blanchet 2010-12-07 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
2010-12-03 hoelzl 2010-12-03 it is known as the extended reals, not the infinite reals
2010-12-06 haftmann 2010-12-06 moved bootstrap of type_lifting to Fun
2010-12-06 haftmann 2010-12-06 replace `type_mapper` by the more adequate `type_lifting`
2010-12-03 wenzelm 2010-12-03 setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
2010-12-01 hoelzl 2010-12-01 Corrected IsaMakefile
2010-12-01 hoelzl 2010-12-01 merged
2010-12-01 hoelzl 2010-12-01 More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
2010-12-01 haftmann 2010-12-01 merged
2010-12-01 haftmann 2010-12-01 file for package tool type_mapper carries the same name as its Isar command
2010-12-01 wenzelm 2010-12-01 activate subtyping/coercions in theory Complex_Main;
2010-12-01 wenzelm 2010-12-01 more precise dependencies;
2010-11-27 huffman 2010-11-27 fix cut-and-paste errors for HOLCF entries in IsaMakefile
2010-11-27 huffman 2010-11-27 moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile;
2010-11-23 haftmann 2010-11-23 merged
2010-11-22 haftmann 2010-11-22 merged
2010-11-22 haftmann 2010-11-22 replaced misleading Fset/fset name -- these do not stand for finite sets
2010-11-22 boehmes 2010-11-22 added prove reconstruction for injective functions; added SMT_Utils to collect frequently used functions