2011-04-14 blanchet 2011-04-14 remove experimental code added in 85bb6fbb8e6a
2011-04-14 blanchet 2011-04-14 added examples of definitional CNF facts
2011-04-14 blanchet 2011-04-14 "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 blanchet 2011-04-14 compile
2011-04-14 blanchet 2011-04-14 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 blanchet 2011-04-14 removed obsolete Skolem counter in new Skolemizer
2011-04-14 blanchet 2011-04-14 added outstanding issue to Metis example
2011-04-14 blanchet 2011-04-14 use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
2011-04-14 blanchet 2011-04-14 started clausifier examples
2011-04-14 blanchet 2011-04-14 make new Skolemizer work also for "metisFT"
2011-04-14 blanchet 2011-04-14 improve definitional CNF on goal by moving "not" past the quantifiers
2011-04-14 blanchet 2011-04-14 experiment with definitional CNF
2011-04-14 blanchet 2011-04-14 use old Skolemizer for Metis call that requires high unification bound (around 100) with the new Skolemizer
2011-04-14 blanchet 2011-04-14 try to repair out-of-sync situations in Metis
2011-04-14 blanchet 2011-04-14 handle Vampire [predicate definition introduction] steps the same way as missing proof, since such steps do not report which axioms were used
2011-04-13 noschinl 2011-04-13 Add YXML.parse_file to signature ...
2011-04-13 noschinl 2011-04-13 Add YXML.parse_file to parse and process big data files
2011-04-13 noschinl 2011-04-13 Generalized File.fold_lines to File.fold_fields
2011-04-11 wenzelm 2011-04-11 more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;
2011-04-11 wenzelm 2011-04-11 Name_Space.entry_markup: keep def position as separate properties; uniform treatment of ML_def/ML_open/ML_struct as entities; hyperlinks for all entities -- excluding ML_open/ML_struct for now;
2011-04-09 wenzelm 2011-04-09 some position reports for 'translations';
2011-04-09 wenzelm 2011-04-09 made SML/NJ happy;
2011-04-09 wenzelm 2011-04-09 merged
2011-04-08 boehmes 2011-04-08 added SMT certificates
2011-04-08 boehmes 2011-04-08 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 boehmes 2011-04-08 fixed eta-expansion: use correct order to apply new bound variables
2011-04-08 boehmes 2011-04-08 check if negating the goal is possible (avoids CTERM exception for Pure propositions)
2011-04-08 boehmes 2011-04-08 unfold and eta-contract let expressions before lambda-lifting to avoid bad terms
2011-04-08 boehmes 2011-04-08 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 bulwahn 2011-04-08 merged
2011-04-08 bulwahn 2011-04-08 deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
2011-04-08 bulwahn 2011-04-08 generalizing instantiate_datatype in quickcheck_exhaustive to remove clones for different compilations
2011-04-08 bulwahn 2011-04-08 correcting constant name in exhaustive_generators
2011-04-08 bulwahn 2011-04-08 switching fast compilation off by default for now in exhaustive quickcheck
2011-04-08 bulwahn 2011-04-08 ensuring datatype limitations before the instantiation in quickcheck_exhaustive
2011-04-08 bulwahn 2011-04-08 rational and real instances for new compilation scheme for exhaustive quickcheck
2011-04-08 bulwahn 2011-04-08 splitting exhaustive and full_exhaustive into separate type classes
2011-04-08 bulwahn 2011-04-08 removing duplicate code
2011-04-08 bulwahn 2011-04-08 revisiting mk_equation functions and refactoring them in exhaustive quickcheck
2011-04-08 bulwahn 2011-04-08 creating a general mk_equation_terms for the different compilations
2011-04-08 bulwahn 2011-04-08 adding an even faster compilation scheme
2011-04-08 bulwahn 2011-04-08 theory definitions for fast exhaustive quickcheck compilation
2011-04-08 bulwahn 2011-04-08 new compilation for exhaustive quickcheck
2011-04-08 wenzelm 2011-04-08 tuned;
2011-04-08 wenzelm 2011-04-08 present type variables; tuned;
2011-04-08 wenzelm 2011-04-08 unparse: more accurate markup for syntax consts, notably binders;
2011-04-08 wenzelm 2011-04-08 notation: proper markup for type constructor / constant;
2011-04-08 wenzelm 2011-04-08 tuned signature;
2011-04-08 wenzelm 2011-04-08 more accurate markup for syntax consts, notably binders which point back to the original logical entity; tuned;
2011-04-08 wenzelm 2011-04-08 discontinued Syntax.max_pri, which is not really a symbolic parameter;
2011-04-08 wenzelm 2011-04-08 CONST syntax with positions;
2011-04-08 wenzelm 2011-04-08 moved CONST syntax/translations to their proper place;
2011-04-08 wenzelm 2011-04-08 simplified Pure syntax bootstrap;
2011-04-08 wenzelm 2011-04-08 renamed sprop "prop#" to "prop'" -- proper identifier; eliminated spurious symbolic string bindings (logic, any etc.); hardwired special "prop" vs. "prop'" conversion; tuned;
2011-04-08 wenzelm 2011-04-08 merged
2011-04-07 krauss 2011-04-07 raised timeout further, for SML/NJ
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2011-04-08 wenzelm 2011-04-08 discontinued special status of structure Printer;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext); clarified Syntax.root;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;