changeset 6112 | 5e4871c5136b |
parent 5505 | b0856ff6fc69 |
child 8551 | 5c22595bc599 |
--- a/src/ZF/QPair.ML Wed Jan 13 11:56:28 1999 +0100 +++ b/src/ZF/QPair.ML Wed Jan 13 11:57:09 1999 +0100 @@ -122,11 +122,9 @@ (*** Eliminator - qsplit ***) (*A META-equality, so that it applies to higher types as well...*) -qed_goalw "qsplit" thy [qsplit_def] - "qsplit(%x y. c(x,y), <a;b>) == c(a,b)" - (fn _ => [ (Simp_tac 1), - (rtac reflexive_thm 1) ]); - +Goalw [qsplit_def] "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"; +by (Simp_tac 1); +qed "qsplit"; Addsimps [qsplit]; qed_goal "qsplit_type" thy