src/HOL/UNITY/UNITY.ML
1999-04-29 paulson 1999-04-29 made many specification operators infix
1999-04-28 paulson 1999-04-28 eliminated theory UNITY/Traces
1999-03-01 paulson 1999-03-01 removed the infernal States, eqStates, compatible, etc.
1998-12-03 paulson 1998-12-03 Addition of the States component; parts of Comp not working
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-19 paulson 1998-10-19 added Clarify_tac to speed up proofs
1998-10-15 paulson 1998-10-15 specifications as sets of programs
1998-10-02 nipkow 1998-10-02 id <-> Id
1998-08-19 paulson 1998-08-19 Misc changes
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-31 paulson 1998-07-31 Tidied; uses records
1998-07-02 paulson 1998-07-02 Uncurried functions LeadsTo and reach Deleted leading parameters thanks to new Goal command
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-03 paulson 1998-04-03 New UNITY theory