equal
deleted
inserted
replaced
117 th''' |
117 th''' |
118 end; |
118 end; |
119 |
119 |
120 fun normalize_equation thy th = |
120 fun normalize_equation thy th = |
121 mk_meta_equation th |
121 mk_meta_equation th |
122 |> Pred_Compile_Set.unfold_set_notation |
122 |> Predicate_Compile_Set.unfold_set_notation |
123 |> full_fun_cong_expand |
123 |> full_fun_cong_expand |
124 |> split_all_pairs thy |
124 |> split_all_pairs thy |
125 |> tap check_equation_format |
125 |> tap check_equation_format |
126 |
126 |
127 fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite |
127 fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite |