src/HOL/UNITY/ELT.thy
2008-05-07 berghofe 2008-05-07 Adapted to encoding of sets as predicates
2008-03-20 haftmann 2008-03-20 tuned proof
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2003-02-27 paulson 2003-02-27 restored some deleted lemmas
2003-02-16 paulson 2003-02-16 minor revisions
2003-02-08 paulson 2003-02-08 converting HOL/UNITY to use unconditional fairness
2003-01-31 paulson 2003-01-31 conversion to new-style theories and tidying
2003-01-29 paulson 2003-01-29 converting UNITY to new-style theories
2001-01-09 nipkow 2001-01-09 *** empty log message ***
2000-10-23 paulson 2000-10-23 quantifiers now allowed in inductive defs
2000-01-14 paulson 2000-01-14 still working; a bit of polishing
2000-01-13 paulson 2000-01-13 working version, with Alloc now working on the same state space as the whole system. Partial removal of ELT.
1999-12-22 paulson 1999-12-22 removing the "{} : CC" requirement for leadsTo[CC]
1999-12-08 paulson 1999-12-08 abolition of localTo: instead "guarantees" has local vars as extra argument
1999-12-01 paulson 1999-12-01 new generalized leads-to theory