src/HOL/Boogie/Tools/boogie_vcs.ML
2010-03-22 boehmes 2010-03-22 provide a hook to safely manipulate verification conditions
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-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-03 boehmes 2009-11-03 added HOL-Boogie