src/HOL/UNITY/UNITY.thy
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2010-05-12 wenzelm 2010-05-12 modernized specifications;
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-03-02 nipkow 2009-03-02 name changes
2007-08-03 wenzelm 2007-08-03 misc cleanup of ML bindings (for multihreading);
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-06-02 paulson 2005-06-02 renamed "constrains" to "safety" to avoid keyword clash
2004-04-22 wenzelm 2004-04-22 constdefs: proper order;
2003-08-15 paulson 2003-08-15 A document for UNITY
2003-03-18 paulson 2003-03-18 moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them to the new Group setup. Deleted Ring, Module from GroupTheory Minor UNITY changes
2003-03-14 paulson 2003-03-14 Proved the main lemma on progress sets
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-30 paulson 2003-01-30 conversion of UNITY theories to new-style
2001-01-09 nipkow 2001-01-09 *** empty log message ***
2001-01-05 nipkow 2001-01-05 ^^ -> ``` Univalent -> single_valued
2000-09-23 paulson 2000-09-23 added compatibility relation: AllowedActs, Allowed, ok, OK and changes to "guarantees", etc.
2000-05-24 paulson 2000-05-24 restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
1999-06-13 paulson 1999-06-13 new-style infix directives
1999-05-24 paulson 1999-05-24 increasing makes sense only for partial orderings
1999-04-29 paulson 1999-04-29 made many specification operators infix
1999-04-28 paulson 1999-04-28 eliminated theory UNITY/Traces
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-08-05 paulson 1998-08-05 New record type of programs
1998-07-13 paulson 1998-07-13 renamed mutex to Acts
1998-04-03 paulson 1998-04-03 New UNITY theory