isabelle: Graph

optimize trivial equalities early in Nitpick -- it shouldn't be the job of the peephole optimizer
2011-04-19, by blanchet
remove a few Nitpick calls in examples -- another step toward making them run faster
2011-04-19, by blanchet
check arity of bound variables to avoid generating too large Kodkod problems -- an issue that arose in the context of TPTP/CASC
2011-04-19, by blanchet
eliminated Codegen.mode in favour of explicit argument;
2011-04-19, by wenzelm
less bulky "_position", for improved readability of parse trees;
2011-04-19, by wenzelm
added more elementary Skip_Proof.make_thm_cterm;
2011-04-19, by wenzelm
explicit markup for loose bounds;
2011-04-19, by wenzelm
prefer internal types, via Simple_Syntax.read_typ;
2011-04-19, by wenzelm
eliminated obsolete Proof_Syntax.strip_sorts_consttypes;
2011-04-19, by wenzelm
split Type_Infer into early and late part, after Proof_Context;
2011-04-19, by wenzelm
minor tuning and modernization;
2011-04-19, by wenzelm
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
2011-04-19, by wenzelm
simplified check/uncheck interfaces: result comparison is hardwired by default;
2011-04-19, by wenzelm
updated some theory primitives, which now depend on auxiliary context;
2011-04-19, by wenzelm
more precise treatment of existing type inference parameters;
2011-04-19, by wenzelm
pretty_abbrev: read abbreviation more directly;
2011-04-18, by wenzelm
tuned signature;
2011-04-18, by wenzelm
raised timeouts further, for SML/NJ!
2011-04-18, by krauss
Package prefix is now taken into account when looking up user-defined
2011-04-18, by berghofe
merged
2011-04-18, by wenzelm
recovered Theory.check_def: full name needs to be determined from background thy, not auxiliary ctxt (broken in 774df7c59508, caused Nitpick.all_axioms_of to produce bad results);
2011-04-18, by wenzelm
scheduler for Mutabelle regression
2011-04-18, by krauss
tool for importing nightly isatest logs
2011-04-18, by krauss
adding bounded_forall tester
2011-04-18, by bulwahn
creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned
2011-04-18, by bulwahn
pass plain Proof.context for pretty printing;
2011-04-18, by wenzelm
standardized aliases of operations on tsig;
2011-04-18, by wenzelm
pass plain Proof.context for pretty printing;
2011-04-18, by wenzelm
tuned;
2011-04-18, by wenzelm
simplified Sorts.class_error: plain Proof.context;
2011-04-18, by wenzelm
pass plain Proof.context for pretty printing;
2011-04-18, by wenzelm
simplified pretty printing context, which is only required for certain kernel operations;
2011-04-18, by wenzelm
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
2011-04-17, by wenzelm
added Binding.print convenience, which includes quote already;
2011-04-17, by wenzelm
markup attributes/methods via name space;
2011-04-17, by wenzelm
tuned signature;
2011-04-17, by wenzelm
markup facts via name space;
2011-04-17, by wenzelm
tuned -- order in memory according to variance;
2011-04-17, by wenzelm
eliminated obsolete markup -- superseded by generic "entity" markup;
2011-04-17, by wenzelm
report Name_Space.declare/define, relatively to context;
2011-04-17, by wenzelm
clarified pretty_parsetree: suppress literal tokens;
2011-04-17, by wenzelm
PARALLEL_GOALS for simplification within auto_tac;
2011-04-16, by wenzelm
PARALLEL_GOALS for method "simp_all";
2011-04-16, by wenzelm
enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);
2011-04-16, by wenzelm
refined PARALLEL_GOALS;
2011-04-16, by wenzelm
tuned blast: navigate to subgoal only once;
2011-04-16, by wenzelm
proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
2011-04-16, by wenzelm
more direct Thm.cprem_of (with exception THM instead of Subscript);
2011-04-16, by wenzelm
more direct Thm.cprem_of (with exception THM instead of Subscript);
2011-04-16, by wenzelm
more direct Logic.dest_implies (with exception TERM instead of Subscript);
2011-04-16, by wenzelm
eliminated old List.nth;
2011-04-16, by wenzelm
do not open ML structures;
2011-04-16, by wenzelm
observe firm naming convention ctxt: Proof.context;
2011-04-16, by wenzelm
modernized structure Proof_Context;
2011-04-16, by wenzelm
modernized structure Proof_Context;
2011-04-16, by wenzelm
prefer local name spaces;
2011-04-16, by wenzelm
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
2011-04-16, by wenzelm
tuned signature, disentangled dependencies;
2011-04-16, by wenzelm
Added command for associating user-defined types with SPARK types.
2011-04-15, by berghofe
turn YXML.parse_file into a fold
2011-04-14, by noschinl
nicer error message from Metis for know failure that isn't the user's fault
2011-04-14, by blanchet
correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"
2011-04-14, by blanchet
tuning
2011-04-14, by blanchet
remove needless export
2011-04-14, by blanchet
more clausification tests
2011-04-14, by blanchet
make 48170228f562 work also with "HO_Reas" examples
2011-04-14, by blanchet
improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)
2011-04-14, by blanchet
properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
2011-04-14, by blanchet
remove experimental code added in 85bb6fbb8e6a
2011-04-14, by blanchet
added examples of definitional CNF facts
2011-04-14, by blanchet
"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
2011-04-14, by blanchet
compile
2011-04-14, by blanchet
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
2011-04-14, by blanchet
removed obsolete Skolem counter in new Skolemizer
2011-04-14, by blanchet
added outstanding issue to Metis example
2011-04-14, by blanchet
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
2011-04-14, by blanchet
started clausifier examples
2011-04-14, by blanchet
make new Skolemizer work also for "metisFT"
2011-04-14, by blanchet
improve definitional CNF on goal by moving "not" past the quantifiers
2011-04-14, by blanchet
experiment with definitional CNF
2011-04-14, by blanchet
use old Skolemizer for Metis call that requires high unification bound (around 100) with the new Skolemizer
2011-04-14, by blanchet
try to repair out-of-sync situations in Metis
2011-04-14, by blanchet
handle Vampire [predicate definition introduction] steps the same way as missing proof, since such steps do not report which axioms were used
2011-04-14, by blanchet
Add YXML.parse_file to signature ...
2011-04-13, by noschinl
Add YXML.parse_file to parse and process big data files
2011-04-13, by noschinl
Generalized File.fold_lines to File.fold_fields
2011-04-13, by noschinl
more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;
2011-04-11, by wenzelm
Name_Space.entry_markup: keep def position as separate properties;
2011-04-11, by wenzelm
some position reports for 'translations';
2011-04-09, by wenzelm
made SML/NJ happy;
2011-04-09, by wenzelm
merged
2011-04-09, by wenzelm
added SMT certificates
2011-04-08, by boehmes
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
2011-04-08, by boehmes
fixed eta-expansion: use correct order to apply new bound variables
2011-04-08, by boehmes
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
2011-04-08, by boehmes
unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
2011-04-08, by boehmes
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
2011-04-08, by boehmes
merged
2011-04-08, by bulwahn
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
2011-04-08, by bulwahn
generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
2011-04-08, by bulwahn
correcting constant name in exhaustive_generators
2011-04-08, by bulwahn
switching fast compilation off by default for now in exhaustive quickcheck
2011-04-08, by bulwahn
ensuring datatype limitations before the instantiation in quickcheck_exhaustive
2011-04-08, by bulwahn
rational and real instances for new compilation scheme for exhaustive quickcheck
2011-04-08, by bulwahn
splitting exhaustive and full_exhaustive into separate type classes
2011-04-08, by bulwahn
removing duplicate code
2011-04-08, by bulwahn
revisiting mk_equation functions and refactoring them in exhaustive quickcheck
2011-04-08, by bulwahn
creating a general mk_equation_terms for the different compilations
2011-04-08, by bulwahn
adding an even faster compilation scheme
2011-04-08, by bulwahn
theory definitions for fast exhaustive quickcheck compilation
2011-04-08, by bulwahn
new compilation for exhaustive quickcheck
2011-04-08, by bulwahn
tuned;
2011-04-08, by wenzelm
present type variables;
2011-04-08, by wenzelm
unparse: more accurate markup for syntax consts, notably binders;
2011-04-08, by wenzelm
notation: proper markup for type constructor / constant;
2011-04-08, by wenzelm
tuned signature;
2011-04-08, by wenzelm
more accurate markup for syntax consts, notably binders which point back to the original logical entity;
2011-04-08, by wenzelm
discontinued Syntax.max_pri, which is not really a symbolic parameter;
2011-04-08, by wenzelm
CONST syntax with positions;
2011-04-08, by wenzelm
moved CONST syntax/translations to their proper place;
2011-04-08, by wenzelm
simplified Pure syntax bootstrap;
2011-04-08, by wenzelm
renamed sprop "prop#" to "prop'" -- proper identifier;
2011-04-08, by wenzelm
merged
2011-04-08, by wenzelm
raised timeout further, for SML/NJ
2011-04-07, by krauss
discontinued special treatment of structure Lexicon;
2011-04-08, by wenzelm
discontinued special status of structure Printer;
2011-04-08, by wenzelm
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
2011-04-08, by wenzelm
discontinued special treatment of structure Mixfix;
2011-04-08, by wenzelm
more antiquotations;
2011-04-08, by wenzelm
removed outdated text (cf. 84a3f86441eb);
2011-04-08, by wenzelm
explicit structure Syntax_Trans;
2011-04-08, by wenzelm
tuned presentation;
2011-04-08, by wenzelm
report literal tokens according to parsetree head;
2011-04-07, by wenzelm
simplified read_term vs. read_prop;
2011-04-07, by wenzelm
tuned signature;
2011-04-07, by wenzelm
constant =?= no longer exists (cf. 8c09e1fa24a7);
2011-04-07, by wenzelm
clarified sources -- removed odd comments;
2011-04-07, by wenzelm
tuned signature;
2011-04-07, by wenzelm
merged
2011-04-07, by wenzelm
removing decrement of cardinality in quickcheck -- counting cardinalities starts at 1
2011-04-07, by bulwahn
removing instantiation exhaustive for unit in Quickcheck_Exhaustive
2011-04-07, by bulwahn
correcting bounded_forall construction; tuned
2011-04-07, by bulwahn
dropped unused lemmas; proper Isar proof
2011-04-07, by haftmann
further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind
2011-04-07, by blanchet
make new Skolemizer more robust
2011-04-07, by blanchet
tuned comment
2011-04-07, by blanchet
discontinued user-defined token translations;
2011-04-07, by wenzelm
simplified printer context: uniform externing and static token translations;
2011-04-07, by wenzelm
clarified Pretty.mark;
2011-04-07, by wenzelm
parallel parsing of big specifications;
2011-04-06, by wenzelm
separate structure Term_Position;
2011-04-06, by wenzelm
type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);
2011-04-06, by wenzelm
moved type syntax translations to syn_trans.ML;
2011-04-06, by wenzelm
made SML/NJ happy (cf. 578a51fae383);
2011-04-06, by wenzelm
merged
2011-04-06, by wenzelm
merged
2011-04-06, by bulwahn
changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)
2011-04-06, by bulwahn
prove measurable_into_infprod_algebra and measure_infprod
2011-04-05, by hoelzl
Rename extensional to extensionalD (extensional is also defined in FuncSet)
2011-04-05, by hoelzl
eliminated slightly odd Syntax.rep_syntax;
2011-04-06, by wenzelm
more abstract print translation;
2011-04-06, by wenzelm
more abstract syntax translation;
2011-04-06, by wenzelm
tuned;
2011-04-06, by wenzelm
explicit Syntax.tokenize, Syntax.parse;
2011-04-06, by wenzelm
eliminated odd object-oriented type_context/term_context;
2011-04-06, by wenzelm
simplified standard parse/unparse;
2011-04-06, by wenzelm
discontinued old-style Syntax.constrainC;
2011-04-06, by wenzelm
typed_print_translation: discontinued show_sorts argument;
2011-04-06, by wenzelm
misc tuning and simplification;
2011-04-06, by wenzelm
moved unparse material to syntax_phases.ML;
2011-04-06, by wenzelm
more symbol abbrevs;
2011-04-06, by wenzelm
renamed Standard_Syntax to Syntax_Phases;
2011-04-06, by wenzelm
moved decode/parse operations to standard_syntax.ML;
2011-04-05, by wenzelm
separate module for standard implementation of inner syntax operations;
2011-04-05, by wenzelm
moved Isar/local_syntax.ML to Syntax/local_syntax.ML;
2011-04-05, by wenzelm
merged
2011-04-05, by wenzelm
added "no_atp" to Cantor's paradox
2011-04-05, by blanchet
renamed "const_args" option value to "args"
2011-04-05, by blanchet
temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception
2011-04-05, by blanchet
updated instructions
2011-04-05, by blanchet
minor doc edits
2011-04-05, by blanchet
killed unimplemented type encoding "preds"
2011-04-05, by blanchet
remove debugging code
2011-04-05, by blanchet
removing bounded_forall code equation for characters when loading Code_Char
2011-04-05, by bulwahn
deriving bounded_forall instances in quickcheck_exhaustive
2011-04-05, by bulwahn
generalizing ensure_sort_datatype for bounded_forall instances
2011-04-05, by bulwahn
document "type_sys" option
2011-04-04, by blanchet
if "monomorphize" is enabled, mangle the type information in the names by default
2011-04-04, by blanchet
use standard tables with standard argument order;
2011-04-05, by wenzelm
discontinued special treatment of structure Parser -- directly accessible;
2011-04-05, by wenzelm
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
2011-04-05, by wenzelm
more precise propagation of reports/results through some inner syntax layers;
2011-04-05, by wenzelm
accumulate parsetrees in canonical reverse order;
2011-04-04, by wenzelm
tuned;
2011-04-04, by wenzelm
tuned -- removed redundancy;
2011-04-04, by wenzelm
tuned signatures;
2011-04-04, by wenzelm
streamlined token list operations, assuming that the order of union does not matter;
2011-04-04, by wenzelm
misc tuning and clarification;
2011-04-04, by wenzelm
merged
2011-04-04, by wenzelm
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
2011-04-04, by blanchet
refactoring generator definition in quickcheck and removing clone
2011-04-04, by bulwahn
use the proper contexts/simpsets/etc. in the TPTP proof method
2011-04-04, by blanchet
merged
2011-04-04, by blanchet
make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option
2011-04-04, by blanchet
merged
2011-04-04, by paulson
Deletion of all semicolons, because they interfere with Proof General
2011-04-04, by paulson
raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
2011-04-04, by krauss
tuned proofs
2011-04-03, by haftmann
tuned proof
2011-04-02, by haftmann
direct pretty printing of parsetrees -- prevent diagnostic output from crashing due to undeclared entities;
2011-04-04, by wenzelm
added Position.reports convenience;
2011-04-03, by wenzelm
show more tooltip/sub-expression markup;
2011-04-03, by wenzelm
show tooltip/sub-expression for entity markup;
2011-04-03, by wenzelm
merged
2011-04-01, by wenzelm
remove unnecessary prob_preserving
2011-04-01, by hoelzl
add prob_space_vimage
2011-04-01, by hoelzl
use Unsynchronized.change convenience, which also emphasizes the raw access to these references (which happen to be local here);
2011-04-01, by wenzelm
fixed accidental redefinition
2011-04-01, by krauss
save reflexivity steps in discharging Z3 Skolemization hypotheses
2011-04-01, by boehmes
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
2011-04-01, by bulwahn
adding general interface for batch validators in quickcheck
2011-04-01, by bulwahn
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
2011-04-01, by blanchet
scheduler for judgement day
2011-04-01, by krauss
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
2011-04-01, by boehmes
make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
2011-04-01, by boehmes
merged
2011-04-01, by bulwahn
adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy
2011-04-01, by bulwahn
raised timeouts further, for SML/NJ
2011-04-01, by krauss
adapted parsing of session timing (cf. e86b10c68f0b)
2011-04-01, by krauss
merged
2011-03-31, by bulwahn
adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
2011-03-31, by bulwahn
provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)
2011-03-31, by boehmes
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
2011-03-31, by blanchet
temporary workaround: filter out spurious monomorphic instances
2011-03-31, by blanchet
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
2011-03-31, by blanchet
added support for "dest:" to "try"
2011-03-31, by blanchet
corrected infix precedence for boolean operators in Haskell
2011-03-31, by haftmann
merged
2011-03-31, by bulwahn
removing dead code in exhaustive_generators
2011-03-30, by bulwahn
removing junk that should not have been committed
2011-03-30, by bulwahn