changeset 5144 | 7ac22e5a05d7 |
parent 5143 | b94cd208f073 |
child 5278 | a903b66822e2 |
--- a/src/HOL/Prod.ML Wed Jul 15 10:15:13 1998 +0200 +++ b/src/HOL/Prod.ML Wed Jul 15 10:58:44 1998 +0200 @@ -155,9 +155,6 @@ "(%(a,b,c,d,e). f(a,b,c,d,e)) = f","(%(a,b,c,d,e,g). f(a,b,c,d,e,g)) = f"]; Addsimps split_etas; (* pragmatic solution *) -Goal "(%(x,y,z).f(x,y,z)) = t"; -by (simp_tac (simpset() addsimps [cond_split_eta]) 1); - qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)" (K [stac surjective_pairing 1, stac split 1, rtac refl 1]);