src/HOL/UNITY/SubstAx.thy
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 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;
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
2003-08-15 paulson 2003-08-15 A document for UNITY
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 converting more UNITY theories to new-style
2000-08-24 paulson 2000-08-24 xsymbols for leads-to and Join
2000-01-13 paulson 2000-01-13 working version, with Alloc now working on the same state space as the whole system. Partial removal of ELT.
1999-11-30 paulson 1999-11-30 working version with new theory ELT
1999-05-04 paulson 1999-05-04 new definitions of Co and LeadsTo
1999-04-29 paulson 1999-04-29 made many specification operators infix
1998-10-15 paulson 1998-10-15 specifications as sets of programs
1998-10-07 paulson 1998-10-07 tidying and renaming
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-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-07-02 paulson 1998-07-02 Uncurried functions LeadsTo and reach Deleted leading parameters thanks to new Goal command
1998-04-03 paulson 1998-04-03 New UNITY theory