src/HOL/Boogie/Boogie.thy
2010-05-12 boehmes 2010-05-12 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
2010-02-11 boehmes 2010-02-11 use full paths when importing theories
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-11-06 boehmes 2009-11-06 tuned
2009-11-05 boehmes 2009-11-05 added references to HOL-Boogie papers
2009-11-03 boehmes 2009-11-03 added HOL-Boogie