| 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
|