src/HOL/SMT_Examples/boogie.ML
Fri, 01 Oct 2021 18:05:19 +0200 wenzelm clarified antiquotations;
Fri, 27 Nov 2020 21:59:23 +0100 wenzelm clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
Sat, 05 Jan 2019 17:24:33 +0100 wenzelm isabelle update -u control_cartouches;
Mon, 24 Sep 2018 16:09:27 +0200 nipkow more conversion from ( * ) to (*)
Thu, 11 Jan 2018 13:48:17 +0100 wenzelm uniform use of Standard ML op-infix -- eliminated warnings;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
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