equal
deleted
inserted
replaced
118 (case Thm.prop_of th of |
118 (case Thm.prop_of th of |
119 Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => |
119 Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => |
120 th RS @{thm eq_reflection} |
120 th RS @{thm eq_reflection} |
121 | _ => th) |
121 | _ => th) |
122 |
122 |
123 val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp} |
123 val meta_fun_cong = @{lemma "\<And>f :: 'a::{} \<Rightarrow> 'b::{}.f == g ==> f x == g x" by simp} |
124 |
124 |
125 fun full_fun_cong_expand th = |
125 fun full_fun_cong_expand th = |
126 let |
126 let |
127 val (f, args) = strip_comb (fst (Logic.dest_equals (Thm.prop_of th))) |
127 val (f, args) = strip_comb (fst (Logic.dest_equals (Thm.prop_of th))) |
128 val i = length (binder_types (fastype_of f)) - length args |
128 val i = length (binder_types (fastype_of f)) - length args |