equal
deleted
inserted
replaced
49 val insts = Thm.first_order_match (concl_pat, concl) |
49 val insts = Thm.first_order_match (concl_pat, concl) |
50 in |
50 in |
51 rtac (Drule.instantiate_normalize insts thm) 1 |
51 rtac (Drule.instantiate_normalize insts thm) 1 |
52 end); |
52 end); |
53 |
53 |
54 fun unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms); |
54 fun unfold_thms_tac _ [] = all_tac |
|
55 | unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms); |
55 |
56 |
56 fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x; |
57 fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x; |
57 |
58 |
58 (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*) |
59 (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*) |
59 fun mk_pointfree ctxt thm = thm |
60 fun mk_pointfree ctxt thm = thm |