Tue, 09 Jan 2001 15:32:27 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
Sat, 23 Sep 2000 16:02:01 +0200 |
paulson |
added compatibility relation: AllowedActs, Allowed, ok,
|
file |
diff |
annotate
|
Fri, 21 Jul 2000 18:01:36 +0200 |
paulson |
much tidying in connection with the 2nd UNITY paper
|
file |
diff |
annotate
|
Wed, 19 Jul 2000 10:59:59 +0200 |
paulson |
deleted redundant proof
|
file |
diff |
annotate
|
Thu, 29 Jun 2000 12:19:27 +0200 |
paulson |
tidied proofs using default rule equalityCE
|
file |
diff |
annotate
|
Fri, 03 Mar 2000 18:26:19 +0100 |
paulson |
Added Tanja's Detects and Reachability theories. Also
|
file |
diff |
annotate
|
Fri, 14 Jan 2000 12:17:53 +0100 |
paulson |
still working; a bit of polishing
|
file |
diff |
annotate
|
Thu, 13 Jan 2000 17:30:23 +0100 |
paulson |
working version, with Alloc now working on the same state space as the whole
|
file |
diff |
annotate
|
Fri, 07 Jan 2000 10:55:35 +0100 |
paulson |
moved some proofs from UNITY/ELT to UNITY/Project
|
file |
diff |
annotate
|
Wed, 22 Dec 1999 17:16:23 +0100 |
paulson |
removing the "{} : CC" requirement for leadsTo[CC]
|
file |
diff |
annotate
|
Tue, 21 Dec 1999 15:03:02 +0100 |
paulson |
working with weak LeadsTo in guarantees precondition\!
|
file |
diff |
annotate
|
Fri, 17 Dec 1999 10:30:48 +0100 |
paulson |
now workign as far as System_Alloc_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, 01 Dec 1999 11:20:24 +0100 |
paulson |
new generalized leads-to theory
|
file |
diff |
annotate
|