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