src/HOL/UNITY/ELT.thy
Mon, 23 Oct 2000 15:20:32 +0200 paulson quantifiers now allowed in inductive defs
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
Wed, 22 Dec 1999 17:16:23 +0100 paulson removing the "{} : CC" requirement for leadsTo[CC]
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