isabelle: Graph

adopting specialisation examples to moving the alternative defs in the library
2010-03-31, by bulwahn
adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
2010-03-31, by bulwahn
no specialisation for predicates without introduction rules in the predicate compiler
2010-03-31, by bulwahn
improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
2010-03-31, by bulwahn
activating the signature of Predicate_Compile again which was deactivated in changeset d93a3cb55068 for debugging purposes
2010-03-31, by bulwahn
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
2010-03-31, by bulwahn
clarifying the Predicate_Compile_Core signature
2010-03-31, by bulwahn
adding signature to Predicate_Compile_Aux; tuning Predicate_Compile_Aux structure
2010-03-31, by bulwahn
putting compilation setup of predicate compiler in a separate file
2010-03-31, by bulwahn
simplify fold_graph proofs
2010-03-30, by huffman
NEWS
2010-03-30, by krauss
removed dead code; fixed typo
2010-03-30, by krauss
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
2010-03-30, by krauss
merged
2010-03-30, by wenzelm
adding skip_proof in the examples because proof procedure cannot handle alternative compilations yet
2010-03-29, by bulwahn
tuned
2010-03-29, by bulwahn
generalized alternative functions to alternative compilation to handle arithmetic functions better
2010-03-29, by bulwahn
correcting alternative functions with tuples
2010-03-29, by bulwahn
no specialisation for patterns with only tuples in the predicate compiler
2010-03-29, by bulwahn
adding registration of functions in the function flattening
2010-03-29, by bulwahn
added book-keeping, registration and compilation with alternative functions for predicates in the predicate compiler
2010-03-29, by bulwahn
adding specialisation examples of the predicate compiler
2010-03-29, by bulwahn
adding specialisation of predicates to the predicate compiler
2010-03-29, by bulwahn
returning an more understandable user error message in the values command
2010-03-29, by bulwahn
adding Lazy_Sequences with explicit depth-bound
2010-03-29, by bulwahn
removing fishing for split thm in the predicate compiler
2010-03-29, by bulwahn
prefer recursive calls before others in the mode inference
2010-03-29, by bulwahn
added statistics to values command for random generation
2010-03-29, by bulwahn
adopting Predicate_Compile_Quickcheck
2010-03-29, by bulwahn
made quickcheck generic with respect to which compilation; added random compilation to quickcheck
2010-03-29, by bulwahn
removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
2010-03-29, by bulwahn
adding a hook for experiments in the predicate compilation process
2010-03-29, by bulwahn
removing simple equalities in introduction rules in the predicate compiler
2010-03-29, by bulwahn
adopting Predicate_Compile
2010-03-29, by bulwahn
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
2010-03-29, by bulwahn
generalizing the compilation process of the predicate compiler
2010-03-29, by bulwahn
added new compilation to predicate_compiler
2010-03-29, by bulwahn
adding new depth-limited and new random monad for the predicate compiler
2010-03-29, by bulwahn
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
2010-03-30, by wenzelm
adapted to Scala 2.8.0 Beta 1;
2010-03-30, by wenzelm
auto update by Netbeans 6.8;
2010-03-30, by wenzelm
adapted to Netbeans 6.8 and Scala for Netbeans 6.8v1.1;
2010-03-30, by wenzelm
replaced some deprecated methods;
2010-03-29, by wenzelm
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
2010-03-29, by wenzelm
merged
2010-03-29, by huffman
use lattice theorems to prove set theorems
2010-03-28, by huffman
add/change some lemmas about lattices
2010-03-28, by huffman
cleaned up some proofs
2010-03-28, by huffman
the configuration option 'trace_simp' now uses the reference of the ProofGeneral settings menu as (dynamic) default value
2010-03-29, by boehmes
merged
2010-03-28, by wenzelm
implicit checkpoint in Local_Theory.theory as well -- no longer export Local_Theory.checkpoint;
2010-03-28, by wenzelm
make SML/NJ happy
2010-03-28, by blanchet
pass raw Context.generic, to avoid wasteful Context.proof_of -- Config.get_thy is often used in performance critical spots like unify.ML;
2010-03-28, by wenzelm
static defaults for configuration options;
2010-03-28, by wenzelm
configuration options admit dynamic default values;
2010-03-28, by wenzelm
tuned;
2010-03-28, by wenzelm
do not export Attrib.register_config, to make it harder to use low-level Config.declare after the bootstrap phase;
2010-03-28, by wenzelm
use regular Attrib.config instead of low-level Config.declare/Attrib.register_config;
2010-03-28, by wenzelm
merged
2010-03-27, by wenzelm
re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
2010-03-27, by boehmes
Typedef.info: separate global and local part, only the latter is transformed by morphisms;
2010-03-27, by wenzelm
merged
2010-03-27, by nipkow
added reference to Trace Simp Depth.
2010-03-27, by nipkow
merged
2010-03-27, by wenzelm
Automated lifting can be restricted to specific quotient types
2010-03-27, by Cezary Kaliszyk
moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;
2010-03-27, by wenzelm
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
2010-03-27, by wenzelm
disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
2010-03-27, by wenzelm
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