TFL/examples/Subst/Unify.ML
1997-02-07 nipkow 1997-02-07 Modified proofs due to added triv_forall_equality.
1996-10-18 paulson 1996-10-18 Subst as modified by Konrad Slind