src/HOL/SMT_Examples/boogie.ML
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT'
Thu, 12 Jun 2014 01:00:49 +0200 blanchet adapted examples to changes in SMT triggers
Thu, 01 May 2014 22:57:38 +0200 boehmes use SMT2 for Boogie examples
Tue, 18 Mar 2014 17:39:03 +0100 wenzelm clarifed module name;
Thu, 27 Feb 2014 17:29:58 +0100 wenzelm store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
Sat, 16 Nov 2013 16:57:09 +0100 wenzelm proper thy_load command 'boogie_file' -- avoid direct access to file-system;
Sat, 27 Jul 2013 16:44:58 +0200 wenzelm tuned spelling;
Sat, 27 Jul 2013 16:35:51 +0200 wenzelm standardized aliases;
Tue, 23 Jul 2013 18:36:23 +0200 boehmes removed obsolete HOL-Boogie session;
less more (0) tip