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
2010-11-22 bulwahn 2010-11-22 adding Enum to HOL-Main image and removing it from HOL-Library
2010-11-22 bulwahn 2010-11-22 adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test
2010-11-22 bulwahn 2010-11-22 adding birthday paradoxon from some abandoned drawer
2010-11-17 haftmann 2010-11-17 module for functorial mappers
2010-11-08 boehmes 2010-11-08 better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
2010-11-08 bulwahn 2010-11-08 adding code and theory for smallvalue generators, but do not setup the interpretation yet
2010-11-04 haftmann 2010-11-04 merged
2010-11-03 haftmann 2010-11-03 moved theory Quicksort from Library/ to ex/
2010-11-04 blanchet 2010-11-04 moved file in makefile to reflect actual dependencies
2010-10-29 wenzelm 2010-10-29 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
2010-10-29 boehmes 2010-10-29 added crafted list of SMT built-in constants
2010-10-28 wenzelm 2010-10-28 moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; tuned;
2010-10-26 blanchet 2010-10-26 reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
2010-10-26 boehmes 2010-10-26 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
2010-10-25 bulwahn 2010-10-25 adding new predicate compiler files to the IsaMakefile
2010-10-25 haftmann 2010-10-25 merged
2010-10-25 haftmann 2010-10-25 moved sledgehammer to Plain; tuned dependencies
2010-10-25 blanchet 2010-10-25 merged
2010-10-25 blanchet 2010-10-25 introduced manual version of "Auto Solve" as "solve_direct"
2010-10-23 krauss 2010-10-23 integrated partial_function into HOL-Plain
2010-10-22 bulwahn 2010-10-22 splitting Hotel Key card example into specification and the two tests for counter example generation
2010-10-22 blanchet 2010-10-22 renamed files
2010-10-05 blanchet 2010-10-05 factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
2010-10-05 blanchet 2010-10-05 factor out "Meson_Tactic" from "Meson_Clausify"
2010-10-04 blanchet 2010-10-04 move Metis into Plain
2010-10-04 blanchet 2010-10-04 added "Meson" theory to Makefile
2010-10-04 blanchet 2010-10-04 move MESON files together
2010-09-29 blanchet 2010-09-29 rename file
2010-09-29 haftmann 2010-09-29 moved old_primrec source to nominal package, where it is still used
2010-09-28 haftmann 2010-09-28 dropped old primrec package
2010-09-28 haftmann 2010-09-28 modernized session
2010-09-27 blanchet 2010-09-27 rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
2010-09-23 bulwahn 2010-09-23 splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
2010-09-20 haftmann 2010-09-20 Factored out ML into separate file
2010-09-17 blanchet 2010-09-17 merged
2010-09-16 blanchet 2010-09-16 added new "Metis_Reconstruct" module, temporarily empty
2010-09-16 blanchet 2010-09-16 rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"