2010-08-08 boehmes 2010-08-08 added scanning of if-then-else expressions
2010-05-26 boehmes 2010-05-26 hide constants and types introduced by SMT, simplified SMT patterns syntax, added examples for SMT patterns
2010-05-12 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-22 wenzelm 2010-03-22 use Specification.axiom, together with Drule.export_without_context that was implicit in the former PureThy.add_axioms (cf. f81557a124d5);
2010-03-22 boehmes 2010-03-22 replaced old-style Drule.add_axiom by Specification.axiomatization
2010-03-22 wenzelm 2010-03-22 replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-18 wenzelm 2010-03-18 typedecl: no sort constraints; prefer Name.invents over old-style Name.variant_list;
2010-03-09 wenzelm 2010-03-09 Typedecl.typedecl_global;
2010-03-07 wenzelm 2010-03-07 separate structure Typedecl;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-26 wenzelm 2010-02-26 tuned;
2010-02-26 wenzelm 2010-02-26 use simplified Syntax.escape;
2010-02-25 boehmes 2010-02-25 use mixfix syntax for Boogie types
2010-02-14 boehmes 2010-02-14 optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program
2010-01-22 boehmes 2010-01-22 drop underscores at end of names coming from Boogie
2009-12-23 boehmes 2009-12-23 merged verification condition structure and term representation in one datatype, extended the set of operations on verification conditions (retrieve more information, advanced splitting of paths), simplified discharging of verification conditions (due to improved datatype), added variantions of commands (extract different parts of verification conditions, scan until first "hard" assertion)
2009-12-11 boehmes 2009-12-11 make assertion labels unique already when loading a verification condition, keep abstract view on verification conditions and provide various splitting operations on verification conditions, allow to discharge only parts of a verification condition, extended the command "boogie_vc" with options to consider only some assertions or to split a verification condition into its paths, added a narrowing option to "boogie_status" (a divide-and-conquer approach for identifying the "hard" subset of assertions of a verification conditions), added tactics "boogie", "boogie_all" and "boogie_cases", dropped tactic "split_vc", split example Boogie_Max into Boogie_Max (proof based on SMT) and Boogie_Max_Stepwise (proof based on metis and auto with documentation of the available Boogie commands), dropped (mostly unused) abbreviations
2009-12-07 boehmes 2009-12-07 verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
2009-11-25 boehmes 2009-11-25 respect "unique" attribute: generate distinctness axioms
2009-11-13 boehmes 2009-11-13 corrected translation of integer operators, keep argument order for n-ary symbols (conjunction, disjunction), removed unused code
2009-11-06 boehmes 2009-11-06 made SML/NJ happy
2009-11-06 boehmes 2009-11-06 tuned
2009-11-05 boehmes 2009-11-05 shorter names for variables and verification conditions, auto-fix variables occurring in a verification condition
2009-11-03 boehmes 2009-11-03 proper and unique case names for the split_vc method, shortened label names, added an example demonstrating the split_vc method
2009-11-03 boehmes 2009-11-03 added HOL-Boogie