src/HOL/Boogie/Tools/boogie_loader.ML
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