src/HOL/UNITY/Union.thy
2003-01-29 paulson 2003-01-29 converted more UNITY theories to new-style
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2000-09-23 paulson 2000-09-23 added compatibility relation: AllowedActs, Allowed, ok, OK and changes to "guarantees", etc.
2000-08-24 paulson 2000-08-24 xsymbols for leads-to and Join
1999-12-08 paulson 1999-12-08 abolition of localTo: instead "guarantees" has local vars as extra argument
1999-10-27 paulson 1999-10-27 working again; new treatment of LocalTo
1999-10-22 paulson 1999-10-22 ALMOST working version: LocalTo results commented out
1999-10-18 paulson 1999-10-18 working version with localTo[C] instead of localTo
1999-10-11 paulson 1999-10-11 working shapshot with "projecting" and "extending"
1999-08-26 paulson 1999-08-26 extra syntax for JN, making it more like UN
1999-03-01 paulson 1999-03-01 removed the infernal States, eqStates, compatible, etc.
1998-12-03 paulson 1998-12-03 Addition of the States component; parts of Comp not working
1998-11-06 paulson 1998-11-06 Revising the Client proof as suggested by Michel Charpentier. New lemmas about composition (in Union.ML), etc. Also changed "length" to "size" because it is displayed as "size" in any event.
1998-10-15 paulson 1998-10-15 specifications as sets of programs
1998-10-05 paulson 1998-10-05 Join now an infix operator
1998-10-01 paulson 1998-10-01 abstype of programs
1998-09-29 paulson 1998-09-29 Now id:(Acts prg) is implicit
1998-08-13 paulson 1998-08-13 Constrains, Stable, Invariant...more of the substitution axiom, but Union does not work well with them
1998-08-05 paulson 1998-08-05 Null program and a few new results
1998-08-05 paulson 1998-08-05 Union primitives and examples