| Wed, 26 Jul 2006 19:23:04 +0200 |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file | diff | annotate |
| Tue, 11 Jul 2006 23:49:32 +0200 |
avoid reference to internal skolem;
|
file | diff | annotate |
| Thu, 22 Dec 2005 00:28:41 +0100 |
mutual induct with *.inducts;
|
file | diff | annotate |
| Fri, 25 Nov 2005 18:58:35 +0100 |
removed obsolete dummy paragraphs;
|
file | diff | annotate |
| Thu, 22 Sep 2005 23:56:15 +0200 |
renamed rules to iprover
|
file | diff | annotate |
| Fri, 17 Jun 2005 16:12:49 +0200 |
migrated theory headers to new format
|
file | diff | annotate |
| Mon, 21 Jun 2004 10:25:57 +0200 |
Merged in license change from Isabelle2004
|
file | diff | annotate |
| Fri, 01 Nov 2002 13:16:28 +0100 |
Inserted some extra paragraphs in large proofs to make tex run...
|
file | diff | annotate |
| Thu, 31 Oct 2002 18:27:10 +0100 |
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
|
file | diff | annotate |
| Mon, 30 Sep 2002 16:14:02 +0200 |
Adapted to new simplifier.
|
file | diff | annotate |
| Tue, 27 Aug 2002 11:03:05 +0200 |
*** empty log message ***
|
file | diff | annotate |
| Tue, 16 Jul 2002 20:25:21 +0200 |
Added conditional and (&&) and or (||).
|
file | diff | annotate |
| Wed, 10 Jul 2002 15:07:02 +0200 |
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
|
file | diff | annotate |
| Fri, 22 Feb 2002 11:26:44 +0100 |
Added check for field/method access to operational semantics and proved the acesses valid.
|
file | diff | annotate |
| Mon, 28 Jan 2002 23:35:20 +0100 |
tuned;
|
file | diff | annotate |
| Mon, 28 Jan 2002 18:50:23 +0100 |
tuned header;
|
file | diff | annotate |
| Mon, 28 Jan 2002 17:00:19 +0100 |
Isabelle/Bali sources;
|
file | diff | annotate |