src/HOL/UNITY/WFair.thy
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