equal
deleted
inserted
replaced
143 val (dx, ndx) = List.partition (contains x) neqs |
143 val (dx, ndx) = List.partition (contains x) neqs |
144 in |
144 in |
145 case ndx of |
145 case ndx of |
146 [] => NONE |
146 [] => NONE |
147 | _ => |
147 | _ => |
148 conj_aci_rule (Thm.mk_binop @{cterm "op \<equiv> :: prop => _"} Pp |
148 conj_aci_rule (Thm.mk_binop @{cterm "(\<equiv>) :: prop => _"} Pp |
149 (Thm.apply @{cterm Trueprop} (list_conj (ndx @ dx)))) |
149 (Thm.apply @{cterm Trueprop} (list_conj (ndx @ dx)))) |
150 |> Thm.abstract_rule xn x |
150 |> Thm.abstract_rule xn x |
151 |> Drule.arg_cong_rule e |
151 |> Drule.arg_cong_rule e |
152 |> Conv.fconv_rule |
152 |> Conv.fconv_rule |
153 (Conv.arg_conv |
153 (Conv.arg_conv |
154 (Simplifier.rewrite |
154 (Simplifier.rewrite |
155 (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps}))) |
155 (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps}))) |
156 |> SOME |
156 |> SOME |
157 end |
157 end |
158 | _ => |
158 | _ => |
159 conj_aci_rule (Thm.mk_binop @{cterm "op \<equiv> :: prop => _"} Pp |
159 conj_aci_rule (Thm.mk_binop @{cterm "(\<equiv>) :: prop => _"} Pp |
160 (Thm.apply @{cterm Trueprop} (list_conj (eqs @ neqs)))) |
160 (Thm.apply @{cterm Trueprop} (list_conj (eqs @ neqs)))) |
161 |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e |
161 |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e |
162 |> Conv.fconv_rule |
162 |> Conv.fconv_rule |
163 (Conv.arg_conv |
163 (Conv.arg_conv |
164 (Simplifier.rewrite |
164 (Simplifier.rewrite |