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