equal
deleted
inserted
replaced
71 end; |
71 end; |
72 |
72 |
73 functor CaseSplitFUN(Data : CASE_SPLIT_DATA) = |
73 functor CaseSplitFUN(Data : CASE_SPLIT_DATA) = |
74 struct |
74 struct |
75 |
75 |
76 val rulify_goals = MetaSimplifier.rewrite_goals_rule Data.rulify; |
76 val rulify_goals = Raw_Simplifier.rewrite_goals_rule Data.rulify; |
77 val atomize_goals = MetaSimplifier.rewrite_goals_rule Data.atomize; |
77 val atomize_goals = Raw_Simplifier.rewrite_goals_rule Data.atomize; |
78 |
78 |
79 (* beta-eta contract the theorem *) |
79 (* beta-eta contract the theorem *) |
80 fun beta_eta_contract thm = |
80 fun beta_eta_contract thm = |
81 let |
81 let |
82 val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm |
82 val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm |