src/HOL/UNITY/Lift.ML
1998-12-11 paulson 1998-12-11 new Close_locale synatx
1998-10-31 paulson 1998-10-31 no need for int_0
1998-10-23 oheimb 1998-10-23 corrected auto_tac (applications of unsafe wrappers)
1998-10-21 wenzelm 1998-10-21 record_split_name;
1998-10-20 wenzelm 1998-10-20 delSWrapper "record_split_tac";
1998-10-15 paulson 1998-10-15 specifications as sets of programs
1998-10-01 paulson 1998-10-01 abstype of programs
1998-09-29 paulson 1998-09-29 modified proof for new simproc
1998-09-25 paulson 1998-09-25 Now uses integers instead of naturals
1998-09-15 paulson 1998-09-15 From Compl(A) to -A
1998-09-14 paulson 1998-09-14 simpler proof
1998-09-11 paulson 1998-09-11 Extra steps at end to make it run faster
1998-09-11 paulson 1998-09-11 fixed PROOF FAILED
1998-09-03 paulson 1998-09-03 A new approach, using simp_of_act and simp_of_set to activate definitions when necessary
1998-09-02 paulson 1998-09-02 modified proofs for new constrains_tac and ensures_tac
1998-09-01 paulson 1998-09-01 Moved lemmas to Arith.ML
1998-08-20 paulson 1998-08-20 New theory Lift
1998-08-19 paulson 1998-08-19 Misc changes
1998-08-14 paulson 1998-08-14 now trans_tac is part of the claset...
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"