src/HOL/SMT_Examples/boogie.ML
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2014-08-28 blanchet 2014-08-28 renamed new SMT module from 'SMT2' to 'SMT'
2014-06-12 blanchet 2014-06-12 adapted examples to changes in SMT triggers
2014-05-01 boehmes 2014-05-01 use SMT2 for Boogie examples
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2014-02-27 wenzelm 2014-02-27 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing; integrity check of SHA1 digests produced in Scala vs. ML; tuned signature;
2013-11-16 wenzelm 2013-11-16 proper thy_load command 'boogie_file' -- avoid direct access to file-system;
2013-07-27 wenzelm 2013-07-27 tuned spelling;
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-07-23 boehmes 2013-07-23 removed obsolete HOL-Boogie session; keep examples that also test SMT solvers, using a minimal version of the old Boogie loader