src/HOL/UNITY/Common.ML
1999-10-11 paulson 1999-10-11 working shapshot with "projecting" and "extending"
1999-09-08 paulson 1999-09-08 now uses the identity function
1999-05-24 paulson 1999-05-24 renamed PSP_stable2->PSP_Stable2
1999-05-04 paulson 1999-05-04 Invariant -> Always and other tidying
1999-04-29 paulson 1999-04-29 made many specification operators infix
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-10-15 paulson 1998-10-15 specifications as sets of programs
1998-10-07 paulson 1998-10-07 tidying and renaming
1998-10-02 nipkow 1998-10-02 id <-> Id
1998-09-29 paulson 1998-09-29 Now id:(Acts prg) is implicit
1998-09-15 paulson 1998-09-15 From Compl(A) to -A
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-08-04 paulson 1998-08-04 Constant "invariant" and new constrains_tac, ensures_tac
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