| Wed, 07 May 2008 10:57:19 +0200 |
berghofe |
Adapted to encoding of sets as predicates
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 12:01:11 +0100 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:46:44 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Thu, 27 Feb 2003 18:21:42 +0100 |
paulson |
restored some deleted lemmas
|
file |
diff |
annotate
|
| Sun, 16 Feb 2003 12:17:40 +0100 |
paulson |
minor revisions
|
file |
diff |
annotate
|
| Sat, 08 Feb 2003 16:05:33 +0100 |
paulson |
converting HOL/UNITY to use unconditional fairness
|
file |
diff |
annotate
|
| Fri, 31 Jan 2003 20:12:44 +0100 |
paulson |
conversion to new-style theories and tidying
|
file |
diff |
annotate
|
| Wed, 29 Jan 2003 11:02:08 +0100 |
paulson |
converting UNITY to new-style theories
|
file |
diff |
annotate
|
| Tue, 09 Jan 2001 15:32:27 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 23 Oct 2000 15:20:32 +0200 |
paulson |
quantifiers now allowed in inductive defs
|
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
|
| Wed, 22 Dec 1999 17:16:23 +0100 |
paulson |
removing the "{} : CC" requirement for leadsTo[CC]
|
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
|