Fri, 18 Feb 2000 15:20:44 +0100 |
paulson |
New treatment of "guarantees" with polymorphic components and bijections.
|
file |
diff |
annotate
|
Wed, 15 Dec 1999 10:45:37 +0100 |
paulson |
first working version to Alloc/System_Client_Progress;
|
file |
diff |
annotate
|
Wed, 08 Dec 1999 13:53:29 +0100 |
paulson |
abolition of localTo: instead "guarantees" has local vars as extra argument
|
file |
diff |
annotate
|
Wed, 27 Oct 1999 13:03:32 +0200 |
paulson |
working again; new treatment of LocalTo
|
file |
diff |
annotate
|
Mon, 11 Oct 1999 10:53:39 +0200 |
paulson |
working shapshot with "projecting" and "extending"
|
file |
diff |
annotate
|
Mon, 04 Oct 1999 13:47:28 +0200 |
paulson |
working snapshot (even Alloc)
|
file |
diff |
annotate
|
Fri, 17 Sep 1999 10:31:38 +0200 |
paulson |
new rule PLam_ensures
|
file |
diff |
annotate
|
Fri, 10 Sep 1999 18:40:06 +0200 |
paulson |
working snapshot
|
file |
diff |
annotate
|
Wed, 08 Sep 1999 15:50:11 +0200 |
paulson |
more rational theorem names (?)
|
file |
diff |
annotate
|
Tue, 31 Aug 1999 15:56:56 +0200 |
paulson |
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
|
file |
diff |
annotate
|
Thu, 26 Aug 1999 11:36:04 +0200 |
paulson |
changed "guar" back to "guarantees" (sorry)
|
file |
diff |
annotate
|
Wed, 25 Aug 1999 11:01:09 +0200 |
paulson |
new guarantees laws; also better natural deduction style for old ones
|
file |
diff |
annotate
|
Fri, 06 Aug 1999 17:29:18 +0200 |
paulson |
re-organization of theorems from Alloc and PPROD, partly into new theory
|
file |
diff |
annotate
|
Thu, 01 Jul 1999 10:36:38 +0200 |
paulson |
expandshort
|
file |
diff |
annotate
|
Wed, 23 Jun 1999 10:39:35 +0200 |
paulson |
renamed PPI to plam
|
file |
diff |
annotate
|
Thu, 17 Jun 1999 10:39:30 +0200 |
paulson |
addition of drop_... operators with new results and simplification of old ones
|
file |
diff |
annotate
|
Sun, 13 Jun 1999 13:55:28 +0200 |
paulson |
many new results for reachable and lift_prog
|
file |
diff |
annotate
|
Mon, 17 May 1999 10:38:08 +0200 |
paulson |
"component" now an infix
|
file |
diff |
annotate
|
Tue, 04 May 1999 13:47:28 +0200 |
paulson |
new definitions of Co and LeadsTo
|
file |
diff |
annotate
|
Thu, 29 Apr 1999 10:51:58 +0200 |
paulson |
made many specification operators infix
|
file |
diff |
annotate
|
Tue, 20 Apr 1999 14:32:48 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
Wed, 03 Mar 1999 10:50:42 +0100 |
paulson |
UNITY fully working at last...
|
file |
diff |
annotate
|
Mon, 01 Mar 1999 18:38:43 +0100 |
paulson |
removed the infernal States, eqStates, compatible, etc.
|
file |
diff |
annotate
|
Mon, 07 Dec 1998 18:26:46 +0100 |
paulson |
towards handling sharing of variables
|
file |
diff |
annotate
|
Thu, 03 Dec 1998 10:45:06 +0100 |
paulson |
Addition of the States component; parts of Comp not working
|
file |
diff |
annotate
|
Wed, 25 Nov 1998 15:55:00 +0100 |
paulson |
guarantees laws
|
file |
diff |
annotate
|
Mon, 16 Nov 1998 13:58:56 +0100 |
paulson |
new theory PPROD
|
file |
diff |
annotate
|