isabelle: Graph

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