isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

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

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle