isabelle: Graph

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
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
move the Sledgehammer Isar commands together into one file;
2010-03-19, by blanchet
more Sledgehammer refactoring
2010-03-19, by blanchet
use a proof context instead of a local theory
2010-03-22, by boehmes
provide a hook to safely manipulate verification conditions
2010-03-22, by boehmes
replaced old-style Drule.add_axiom by Specification.axiomatization
2010-03-22, by boehmes
removed e-mail address from error message
2010-03-22, by boehmes
merged
2010-03-22, by haftmann
tuned whitespace
2010-03-21, by haftmann
handle hidden polymorphism in class target (without class target syntax, though)
2010-03-21, by haftmann
replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
2010-03-22, by wenzelm
replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-22, by wenzelm
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
2010-03-21, by wenzelm
Logic.mk_of_sort convenience;
2010-03-21, by wenzelm
more explicit invented name;
2010-03-21, by wenzelm
minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
2010-03-21, by wenzelm
do not open ML structures;
2010-03-21, by wenzelm
modernized overloaded definitions;
2010-03-21, by wenzelm
standard headers;
2010-03-21, by wenzelm
slightly more uniform definitions -- eliminated old-style meta-equality;
2010-03-21, by wenzelm
eliminated old constdefs;
2010-03-21, by wenzelm
corrected setup for of_list
2010-03-21, by haftmann
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-20, by wenzelm
added lemma infinite_Un
2010-03-20, by Christian Urban
Check that argument is not a 'Bound' before calling fastype_of.
2010-03-19, by Cezary Kaliszyk
typedef etc.: no constraints;
2010-03-19, by wenzelm
allow sort constraints in HOL/typedef;
2010-03-19, by wenzelm
allow sort constraints in HOL/typedef and related HOLCF variants;
2010-03-19, by wenzelm
OuterParse.type_args_constrained;
2010-03-19, by wenzelm
support type arguments with sort constraints;
2010-03-19, by wenzelm
typedecl: no sort constraints;
2010-03-18, by wenzelm
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints;
2010-03-18, by wenzelm
typedecl: no sort constraints;
2010-03-18, by wenzelm
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
2010-03-18, by wenzelm
Added product measure space
2010-03-16, by hoelzl
added type constraints to make SML/NJ happy
2010-03-18, by blanchet
merged
2010-03-18, by blanchet
fix Mirabelle after renaming Sledgehammer structures
2010-03-18, by blanchet
merged
2010-03-18, by blanchet
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-18, by blanchet
renamed "ATP_Linkup" theory to "Sledgehammer"
2010-03-17, by blanchet
renamed Sledgehammer structures
2010-03-17, by blanchet
move Sledgehammer files in a directory of their own
2010-03-17, by blanchet
merged
2010-03-18, by haftmann
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-18, by haftmann
lemma swap_inj_on, swap_product
2010-03-18, by haftmann
meaningful transfer certificate
2010-03-18, by haftmann
dropped odd interpretation of comm_monoid_mult into comm_monoid_add; consider Min.insert_idem as default simp rule
2010-03-18, by haftmann
updated certificate
2010-03-18, by haftmann
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-18, by haftmann
added locales folding_one_(idem); various streamlining and tuning
2010-03-18, by haftmann
generic locale for big operators in monoids; dropped odd interpretation of comm_monoid_mult into comm_monoid_add
2010-03-18, by haftmann
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
2010-03-17, by boehmes
added one-entry cache around Kodkod invocation
2010-03-17, by blanchet
merged
2010-03-17, by blanchet
solve error in "Nitpick_Mono" + short path when no finite functions are inferred
2010-03-17, by blanchet
minor additions to Nitpick docs
2010-03-17, by blanchet
NEWS: Nat_Bijection library
2010-03-17, by huffman
document "nitpick_choice_spec" attribute
2010-03-17, by blanchet
fix typo in "nitpick_choice_spec" attribute name (singular, not plural)
2010-03-17, by blanchet
added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-17, by blanchet
rollback of local typedef until problem with type-variables can be sorted out; fixed header
2010-03-16, by Christian Urban
adjusted to changes in Finite_Set
2010-03-16, by haftmann
merged
2010-03-15, by wenzelm
merged
2010-03-15, by nipkow
tuned inductions
2010-03-15, by nipkow
tuned;
2010-03-15, by wenzelm
moved old Sign.intern_term to the place where it is still used;
2010-03-15, by wenzelm
preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
2010-03-15, by wenzelm
replaced type_syntax/term_syntax by uniform syntax_declaration;
2010-03-15, by wenzelm
merged
2010-03-15, by haftmann
corrected disastrous syntax declarations
2010-03-15, by haftmann
added stmaryrd for isasymSqinter
2010-03-15, by haftmann
use headers consistently
2010-03-14, by huffman
no_document for theory Countable
2010-03-14, by huffman
old domain package also defines map functions
2010-03-14, by huffman
separate map-related code into new function define_map_functions
2010-03-14, by huffman
removed Local_Theory.theory_result by using local Typedef.add_typedef
2010-03-14, by Christian Urban
tuned comment;
2010-03-14, by wenzelm
observe standard header format;
2010-03-14, by wenzelm
expose formal text;
2010-03-14, by wenzelm
localized @{class} and @{type};
2010-03-14, by wenzelm
move functions into holcf_library.ML
2010-03-14, by huffman
simplify definition of when combinators
2010-03-14, by huffman
declare case_names for various induction rules
2010-03-13, by huffman