equal
deleted
inserted
replaced
24 by (rtac refl 1); |
24 by (rtac refl 1); |
25 qed "pair_eta_expand"; |
25 qed "pair_eta_expand"; |
26 |
26 |
27 local |
27 local |
28 val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))]; |
28 val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))]; |
29 val rew = mk_meta_eq pair_eta_expand; |
29 val rew = meta_eq pair_eta_expand; |
30 |
30 |
31 fun proc _ _ (Abs _) = Some rew |
31 fun proc _ _ (Abs _) = Some rew |
32 | proc _ _ _ = None; |
32 | proc _ _ _ = None; |
33 in |
33 in |
34 val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc; |
34 val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc; |