equal
deleted
inserted
replaced
51 |
51 |
52 fun norm_def thm = |
52 fun norm_def thm = |
53 (case Thm.prop_of thm of |
53 (case Thm.prop_of thm of |
54 \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Abs _) => |
54 \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Abs _) => |
55 norm_def (thm RS @{thm fun_cong}) |
55 norm_def (thm RS @{thm fun_cong}) |
56 | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq}) |
56 | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ Abs _ => norm_def (HOLogic.mk_obj_eq thm) |
57 | _ => thm) |
57 | _ => thm) |
58 |
58 |
59 |
59 |
60 (** atomization **) |
60 (** atomization **) |
61 |
61 |