equal
deleted
inserted
replaced
151 by (rule exchLS) |
151 by (rule exchLS) |
152 |
152 |
153 ML {* |
153 ML {* |
154 (*Cut and thin, replacing the right-side formula*) |
154 (*Cut and thin, replacing the right-side formula*) |
155 fun cutR_tac ctxt s i = |
155 fun cutR_tac ctxt s i = |
156 Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s) ] @{thm cut} i THEN |
156 Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN |
157 rtac @{thm thinR} i |
157 rtac @{thm thinR} i |
158 |
158 |
159 (*Cut and thin, replacing the left-side formula*) |
159 (*Cut and thin, replacing the left-side formula*) |
160 fun cutL_tac ctxt s i = |
160 fun cutL_tac ctxt s i = |
161 Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] @{thm cut} i THEN |
161 Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN |
162 rtac @{thm thinL} (i + 1) |
162 rtac @{thm thinL} (i + 1) |
163 *} |
163 *} |
164 |
164 |
165 |
165 |
166 (** If-and-only-if rules **) |
166 (** If-and-only-if rules **) |