src/HOL/UNITY/Union.thy
2016-05-25 wenzelm 2016-05-25 isabelle update_cartouches -c -t;
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2015-12-27 wenzelm 2015-12-27 discontinued ASCII replacement syntax <->;
2015-07-23 wenzelm 2015-07-23 more symbols by default, without xsymbols mode;
2015-06-26 wenzelm 2015-06-26 proper spacing, as for other syntax for these symbols;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-03-22 haftmann 2014-03-22 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
2012-02-21 wenzelm 2012-02-21 tuned proofs;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2010-05-12 wenzelm 2010-05-12 modernized specifications;
2010-03-03 wenzelm 2010-03-03 notation for xsymbols (cf. ad039d29e01c);
2010-03-02 wenzelm 2010-03-02 proper (type_)notation;
2010-02-10 wenzelm 2010-02-10 modernized translations;
2010-02-08 wenzelm 2010-02-08 modernized some syntax translations;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-03-05 haftmann 2009-03-05 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2005-08-01 wenzelm 2005-08-01 no eq_commute;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2003-08-15 paulson 2003-08-15 A document for UNITY
2003-02-16 paulson 2003-02-16 minor revisions
2003-02-08 paulson 2003-02-08 converting HOL/UNITY to use unconditional fairness
2003-02-04 paulson 2003-02-04 some x-symbols
2003-01-31 paulson 2003-01-31 conversion to new-style theories and tidying
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