src/HOL/UNITY/WFair.thy
2015-07-23 wenzelm 2015-07-23 more symbols by default, without xsymbols mode;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-11-12 wenzelm 2011-11-12 tuned proofs;
2011-08-09 haftmann 2011-08-09 tuned proofs
2010-07-22 wenzelm 2010-07-22 updated some headers;
2010-03-01 wenzelm 2010-03-01 tuned final whitespace;
2010-03-01 haftmann 2010-03-01 merged
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-24 wenzelm 2010-02-24 modernized syntax declarations, and make them actually work with authentic syntax;
2009-09-21 haftmann 2009-09-21 tuned proofs
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2006-06-05 krauss 2006-06-05 Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". This simplifies some proofs.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-07-15 nipkow 2004-07-15 Moved to new m<..<n syntax for set intervals.
2003-08-15 paulson 2003-08-15 A document for UNITY
2003-07-15 paulson 2003-07-15 tidying
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-10-23 paulson 2000-10-23 quantifiers now allowed in inductive defs
2000-08-24 paulson 2000-08-24 xsymbols for leads-to and Join
1999-11-11 paulson 1999-11-11 tidied
1999-08-25 paulson 1999-08-25 arguably clearer definition of the inductive case of leads-to. No proofs had to be changed...
1999-06-08 paulson 1999-06-08 renamed the underlying relation of leadsTo from "leadsto" to "leads" to reduce the risk of confusion
1999-04-29 paulson 1999-04-29 made many specification operators infix
1998-11-18 paulson 1998-11-18 Finally removing "Compl" from HOL
1998-10-21 berghofe 1998-10-21 Changed interface of inductive.
1998-10-15 paulson 1998-10-15 specifications as sets of programs
1998-08-19 paulson 1998-08-19 Misc changes
1998-08-06 paulson 1998-08-06 A higher-level treatment of LeadsTo, minimizing use of "reachable"
1998-08-05 paulson 1998-08-05 New record type of programs
1998-08-04 paulson 1998-08-04 Tidying
1998-07-17 paulson 1998-07-17 added comments
1998-04-03 paulson 1998-04-03 New UNITY theory