src/HOL/UNITY/Union.thy
Thu, 23 Jul 2015 22:13:42 +0200 wenzelm more symbols by default, without xsymbols mode;
Fri, 26 Jun 2015 11:07:04 +0200 wenzelm proper spacing, as for other syntax for these symbols;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sat, 22 Mar 2014 08:37:43 +0100 haftmann generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
Tue, 21 Feb 2012 17:09:17 +0100 wenzelm tuned proofs;
Sun, 20 Nov 2011 21:05:23 +0100 wenzelm eliminated obsolete "standard";
Wed, 14 Sep 2011 10:08:52 -0400 hoelzl renamed Complete_Lattices lemmas, removed legacy names
Wed, 12 May 2010 16:44:49 +0200 wenzelm modernized specifications;
Wed, 03 Mar 2010 12:02:59 +0100 wenzelm notation for xsymbols (cf. ad039d29e01c);
Tue, 02 Mar 2010 23:59:54 +0100 wenzelm proper (type_)notation;
Wed, 10 Feb 2010 00:46:56 +0100 wenzelm modernized translations;
Mon, 08 Feb 2010 21:28:27 +0100 wenzelm modernized some syntax translations;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Thu, 05 Mar 2009 08:23:11 +0100 haftmann set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
Mon, 01 Aug 2005 19:20:31 +0200 wenzelm no eq_commute;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Fri, 15 Aug 2003 13:07:01 +0200 paulson A document for UNITY
Sun, 16 Feb 2003 12:17:40 +0100 paulson minor revisions
Sat, 08 Feb 2003 16:05:33 +0100 paulson converting HOL/UNITY to use unconditional fairness
Tue, 04 Feb 2003 18:12:40 +0100 paulson some x-symbols
Fri, 31 Jan 2003 20:12:44 +0100 paulson conversion to new-style theories and tidying
Wed, 29 Jan 2003 16:34:51 +0100 paulson converted more UNITY theories to new-style
Fri, 09 Nov 2001 00:09:47 +0100 wenzelm eliminated old "symbols" syntax, use "xsymbols" instead;
Sat, 23 Sep 2000 16:02:01 +0200 paulson added compatibility relation: AllowedActs, Allowed, ok,
Thu, 24 Aug 2000 12:39:24 +0200 paulson xsymbols for leads-to and Join
Wed, 08 Dec 1999 13:53:29 +0100 paulson abolition of localTo: instead "guarantees" has local vars as extra argument
Wed, 27 Oct 1999 13:03:32 +0200 paulson working again; new treatment of LocalTo
Fri, 22 Oct 1999 18:35:20 +0200 paulson ALMOST working version: LocalTo results commented out
Mon, 18 Oct 1999 15:18:24 +0200 paulson working version with localTo[C] instead of localTo
Mon, 11 Oct 1999 10:53:39 +0200 paulson working shapshot with "projecting" and "extending"
Thu, 26 Aug 1999 11:33:24 +0200 paulson extra syntax for JN, making it more like UN
Mon, 01 Mar 1999 18:38:43 +0100 paulson removed the infernal States, eqStates, compatible, etc.
Thu, 03 Dec 1998 10:45:06 +0100 paulson Addition of the States component; parts of Comp not working
Fri, 06 Nov 1998 13:20:29 +0100 paulson Revising the Client proof as suggested by Michel Charpentier. New lemmas
Thu, 15 Oct 1998 11:35:07 +0200 paulson specifications as sets of programs
Mon, 05 Oct 1998 10:22:49 +0200 paulson Join now an infix operator
Thu, 01 Oct 1998 18:28:18 +0200 paulson abstype of programs
Tue, 29 Sep 1998 15:58:47 +0200 paulson Now id:(Acts prg) is implicit
Thu, 13 Aug 1998 18:06:40 +0200 paulson Constrains, Stable, Invariant...more of the substitution axiom, but Union
Wed, 05 Aug 1998 18:21:37 +0200 paulson Null program and a few new results
Wed, 05 Aug 1998 10:56:58 +0200 paulson Union primitives and examples
less more (0) tip