| Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:04 +0200 |
boehmes |
introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
| Sun, 08 Aug 2010 04:28:51 +0200 |
boehmes |
added scanning of if-then-else expressions
|
file |
diff |
annotate
|
| Wed, 26 May 2010 15:34:47 +0200 |
boehmes |
hide constants and types introduced by SMT,
|
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
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 19:25:14 +0100 |
wenzelm |
use Specification.axiom, together with Drule.export_without_context that was implicit in the former PureThy.add_axioms (cf. f81557a124d5);
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 09:40:11 +0100 |
boehmes |
replaced old-style Drule.add_axiom by Specification.axiomatization
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 00:48:56 +0100 |
wenzelm |
replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 23:08:52 +0100 |
wenzelm |
typedecl: no sort constraints;
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 23:32:49 +0100 |
wenzelm |
Typedecl.typedecl_global;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:47:02 +0100 |
wenzelm |
separate structure Typedecl;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Fri, 26 Feb 2010 23:07:27 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 26 Feb 2010 23:05:47 +0100 |
wenzelm |
use simplified Syntax.escape;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 09:16:16 +0100 |
boehmes |
use mixfix syntax for Boogie types
|
file |
diff |
annotate
|
| Sun, 14 Feb 2010 17:46:28 +0100 |
boehmes |
optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program
|
file |
diff |
annotate
|
| Fri, 22 Jan 2010 16:33:44 +0100 |
boehmes |
drop underscores at end of names coming from Boogie
|
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
|
| Mon, 07 Dec 2009 09:12:16 +0100 |
boehmes |
verbose output of loaded data makes a clear distinction between new and already existing data (types, constants, axioms)
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 12:28:29 +0100 |
boehmes |
respect "unique" attribute: generate distinctness axioms
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 15:06:19 +0100 |
boehmes |
corrected translation of integer operators,
|
file |
diff |
annotate
|
| Fri, 06 Nov 2009 21:53:20 +0100 |
boehmes |
made SML/NJ happy
|
file |
diff |
annotate
|
| Fri, 06 Nov 2009 09:27:20 +0100 |
boehmes |
tuned
|
file |
diff |
annotate
|
| Thu, 05 Nov 2009 14:48:40 +0100 |
boehmes |
shorter names for variables and verification conditions,
|
file |
diff |
annotate
|
| Tue, 03 Nov 2009 23:44:16 +0100 |
boehmes |
proper and unique case names for the split_vc method,
|
file |
diff |
annotate
|
| Tue, 03 Nov 2009 17:54:24 +0100 |
boehmes |
added HOL-Boogie
|
file |
diff |
annotate
|