src/HOL/SMT_Examples/SMT_Word_Examples.thy
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Thu, 26 May 2016 17:51:22 +0200 wenzelm isabelle update_cartouches -c -t;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sun, 21 Sep 2014 16:56:11 +0200 haftmann explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
Thu, 18 Sep 2014 00:03:46 +0200 blanchet renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renamed new SMT module from 'SMT2' to 'SMT'
Thu, 13 Mar 2014 14:55:38 +0100 blanchet updated SMT example certificates
Thu, 13 Mar 2014 13:18:13 +0100 blanchet use 'smt2' in SMT examples as much as currently possible
Tue, 11 Mar 2014 15:34:38 +0100 blanchet full path
Tue, 27 Mar 2012 16:59:13 +0300 blanchet renamed "smt_fixed" to "smt_read_only_certificates"
Mon, 17 Jan 2011 17:45:52 +0100 boehmes made Z3 the default SMT solver again
Sun, 19 Dec 2010 18:55:21 +0100 boehmes updated SMT certificates
Fri, 12 Nov 2010 15:56:07 +0100 boehmes look for certificates relative to the theory
Tue, 26 Oct 2010 11:46:19 +0200 boehmes changed SMT configuration options; updated SMT certificates
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
less more (0) tip