| Thu, 23 Aug 2012 15:06:15 +0200 |
wenzelm |
turned 'boogie_open' into thy_load command, without any declarations of 'uses';
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 23:41:16 +0200 |
wenzelm |
tuned Named_Thms: proper binding;
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:04 +0200 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 09:14:08 +0100 |
boehmes |
use full paths when importing theories
|
file |
diff |
annotate
|
| Wed, 23 Dec 2009 17:35:56 +0100 |
boehmes |
merged verification condition structure and term representation in one datatype,
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 15:35:29 +0100 |
boehmes |
make assertion labels unique already when loading a verification condition,
|
file |
diff |
annotate
|
| Fri, 06 Nov 2009 09:27:20 +0100 |
boehmes |
tuned
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 14:41:37 +0100 |
boehmes |
added references to HOL-Boogie papers
|
file |
diff |
annotate
|
| Tue, 03 Nov 2009 17:54:24 +0100 |
boehmes |
added HOL-Boogie
|
file |
diff |
annotate
|