2010-03-27 wenzelm added Term.fold_atyps_sorts convenience;
2010-03-27 wenzelm moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
2010-03-27 wenzelm eliminated old-style Theory.add_defs_i;
2010-03-27 boehmes slightly more general simproc (avoids errors of linarith)
2010-03-26 boehmes merged
2010-03-26 boehmes updated SMT certificates
2010-03-26 boehmes made renamings stable under name changes in the original problem (uninterpreted names are irrelevant to the SMT solver, and caching of SMT certificates relies on irrelevancy of renamings)
2010-03-26 boehmes replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
2010-03-26 wenzelm merged
2010-03-26 hoelzl Added finite measure space.
2010-03-26 wenzelm tuned white space;
2010-03-26 wenzelm more efficient merge_algebra for important special cases -- tricky due to required completion if class algebra changes;
2010-03-26 wenzelm low-level tuning for join/merge: ignore identical versions (SUBTLE CHANGE IN SEMANTICS);
2010-03-25 wenzelm merged
2010-03-25 blanchet merged
2010-03-25 blanchet make Mirabelle happy again
2010-03-24 blanchet revert debugging output that shouldn't have been submitted in the first place
2010-03-24 blanchet added support for Sledgehammer parameters;
2010-03-24 blanchet simplify Nitpick parameter parsing code a little bit + make compile
2010-03-24 blanchet add new file "sledgehammer_util.ML" to setup
2010-03-24 blanchet honor the newly introduced Sledgehammer parameters and fixed the parsing;
2010-03-23 blanchet added a syntax for specifying facts to Sledgehammer;
2010-03-23 blanchet leverage code now in Sledgehammer
2010-03-23 blanchet added options to Sledgehammer;
2010-03-22 blanchet make "sledgehammer" and "atp_minimize" improper commands
2010-03-25 wenzelm Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
2010-03-25 wenzelm removed unused AxClass.of_sort derivation;
2010-03-24 wenzelm more precise dependencies;
2010-03-24 wenzelm merged
2010-03-24 bulwahn merged
2010-03-24 bulwahn removed predicate_compile_core.ML from HOL-ex session
2010-03-24 bulwahn added predicate compiler quickcheck examples to new session Predicate_Compile_Examples
2010-03-24 bulwahn adopting examples to Library move
2010-03-24 bulwahn moved further predicate compile files to HOL-Library
2010-03-24 bulwahn added simple setup for arithmetic on natural numbers
2010-03-24 bulwahn removing uncommented examples in setup theory of predicate compile quickcheck
2010-03-24 bulwahn moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
2010-03-24 wenzelm slightly more logical bootstrap order -- also helps to sort out proof terms extension;
2010-03-24 huffman remove ancient continuity tactic
2010-03-24 boehmes removed Cache_IO component
2010-03-24 boehmes updated SMT certificates
2010-03-24 boehmes inhibit invokation of external SMT solver
2010-03-24 boehmes more precise dependencies
2010-03-24 boehmes cache_io is now just a single ML file instead of a component
2010-03-24 boehmes use internal SHA1 digest implementation for generating hash keys
2010-03-24 boehmes remove component Cache_IO (external dependency on MD5 will be replaced by internal SHA1 digest implementation)
2010-03-24 huffman merged
2010-03-23 huffman minimize dependencies
2010-03-23 huffman sublocale comm_monoid_add < setprod --> sublocale comm_monoid_mult < setprod
2010-03-23 boehmes use ml_platform instead of ml_system to distinguish library names
2010-03-23 boehmes merged
2010-03-23 boehmes use LONG rather than INT to represent the C datatype size_t
2010-03-23 wenzelm merged
2010-03-23 huffman remove continuous let-binding function CLet; add cont2cont rule ordinary Let
2010-03-23 huffman move letrec stuff to new file HOLCF/ex/Letrec.thy
2010-03-23 wenzelm more accurate dependencies;
2010-03-23 wenzelm even less ambitious isatest for smlnj;
2010-03-23 hoelzl Unhide measure_space.positive defined in Caratheodory.
2010-03-23 hoelzl Generate image for HOL-Probability
2010-03-23 wenzelm updated Thm.add_axiom/add_def;
2010-03-23 huffman completely remove constants cpair, cfst, csnd
2010-03-23 huffman use Pair instead of cpair in Fixrec_ex.thy
2010-03-23 huffman use Pair instead of cpair
2010-03-23 huffman define CLetrec using Pair, fst, snd instead of cpair, cfst, csnd
2010-03-23 huffman define csplit using fst, snd
2010-03-23 huffman convert lemma fix_cprod to use Pair, fst, snd
2010-03-23 huffman remove unused syntax for as_pat, lazy_pat
2010-03-23 huffman add lemmas fst_monofun, snd_monofun
2010-03-23 huffman use Pair instead of cpair
2010-03-23 huffman use fixrec_simp instead of fixpat
2010-03-23 huffman use Pair, fst, snd instead of cpair, cfst, csnd
2010-03-23 huffman remove admw predicate
2010-03-23 huffman remove contlub predicate
2010-03-22 huffman merged
2010-03-22 huffman error -> raise Fail
2010-03-22 wenzelm merged
2010-03-22 wenzelm merged
2010-03-22 wenzelm merged
2010-03-22 huffman remove unused adm_tac.ML
2010-03-22 huffman avoid dependence on adm_tac solver
2010-03-22 huffman remove obsolete holcf_logic.ML
2010-03-22 huffman fix ML warning in domain_library.ML
2010-03-22 huffman fix ML warnings in repdef.ML
2010-03-22 huffman fix ML warnings in fixrec.ML
2010-03-22 huffman fix ML warnings in pcpodef.ML
2010-03-22 huffman fix LaTeX overfull hbox warnings in HOLCF document
2010-03-22 huffman remove LaTeX hyperref warnings by avoiding antiquotations within section headings
2010-03-22 wenzelm explicit Simplifier.global_context;
2010-03-22 wenzelm recovered header;
2010-03-22 wenzelm eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
2010-03-22 wenzelm inlined version of old-style Drule.add_axioms -- Specification.axiom is not bootstrapped yet;
2010-03-22 wenzelm use Specification.axiom, together with Drule.export_without_context that was implicit in the former PureThy.add_axioms (cf. f81557a124d5);
2010-03-22 wenzelm added Specification.axiom convenience;
2010-03-22 blanchet detect OFCLASS() axioms in Nitpick;
2010-03-22 bulwahn merged
2010-03-22 bulwahn contextifying the compilation of the predicate compiler
2010-03-22 bulwahn removed unused Predicate_Compile_Set
2010-03-22 bulwahn avoiding fishing for split_asm rule in the predicate compiler
2010-03-22 bulwahn contextifying the proof procedure in the predicate compiler
2010-03-22 bulwahn making flat triples to nested tuple to remove general triple functions
2010-03-22 bulwahn reduced the debug output functions from 2 to 1
2010-03-22 bulwahn some improvements thanks to Makarius source code review
2010-03-22 bulwahn adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
2010-03-22 bulwahn enabling a previously broken example of the predicate compiler again
2010-03-22 bulwahn improving handling of case expressions in predicate rewriting
2010-03-22 bulwahn adding depth_limited_random compilation to predicate compiler
2010-03-22 bulwahn a new simpler random compilation for the predicate compiler
2010-03-22 bulwahn reviving the classical depth-limited computation in the predicate compiler
2010-03-22 bulwahn cleaning the function flattening
2010-03-22 bulwahn generalized split transformation in the function flattening
2010-03-22 bulwahn only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
2010-03-22 bulwahn restructuring function flattening
2010-03-22 bulwahn renaming mk_prems to flatten in the function flattening
2010-03-22 bulwahn simplifying function flattening
2010-03-22 boehmes removed warning_count (known causes for warnings have been resolved)
2010-03-22 blanchet remove the iteration counter from Sledgehammer's minimizer
2010-03-22 blanchet merged
2010-03-22 blanchet start work on direct proof reconstruction for Sledgehammer
2010-03-19 blanchet renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
2010-03-19 blanchet move all ATP setup code into ATP_Wrapper
(0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip