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