src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
Tue, 01 Jan 2013 11:36:30 +0100 blanchet regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
Thu, 23 Aug 2012 15:06:15 +0200 wenzelm turned 'boogie_open' into thy_load command, without any declarations of 'uses';
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
Thu, 06 Jan 2011 17:51:56 +0100 boehmes differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
Wed, 17 Nov 2010 09:22:23 +0100 boehmes require the b2i file ending in the boogie_open command (for consistency with the theory header)
Mon, 15 Nov 2010 00:20:36 +0100 boehmes formal dependency on b2i files
less more (0) -10 -7 tip