src/HOL/Subst/Unify.ML
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-03 nipkow 1998-07-03 Removed leading !! in goals
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-03 nipkow 1997-11-03 expand_option_case -> split_option_case
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-09-29 paulson 1997-09-29 Step_tac -> Safe_tac
1997-06-03 paulson 1997-06-03 No longer refers to internal TFL structures
1997-05-26 paulson 1997-05-26 Simplified proofs using expand_option_case
1997-05-22 paulson 1997-05-22 Now uses type option instead of Fail/Subst No references to wf_rel_prod
1997-05-21 paulson 1997-05-21 Removed rprod from the WF relation; simplified proofs; induction rule is now curried
1997-05-20 paulson 1997-05-20 Removal of duplicate code from TFL
1997-05-16 oheimb 1997-05-16 renamed unsafe_addss to addss
1997-05-15 paulson 1997-05-15 New version, modified by Konrad Slind and LCP for TFL