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 res_inst_tac ctxt [((("P", 0), Position.none), s) ] @{thm cut} i THEN rtac @{thm thinR} i |
156 Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s) ] @{thm cut} i THEN |
|
157 rtac @{thm thinR} i |
157 |
158 |
158 (*Cut and thin, replacing the left-side formula*) |
159 (*Cut and thin, replacing the left-side formula*) |
159 fun cutL_tac ctxt s i = |
160 fun cutL_tac ctxt s i = |
160 res_inst_tac ctxt [((("P", 0), Position.none), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1) |
161 Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] @{thm cut} i THEN |
|
162 rtac @{thm thinL} (i + 1) |
161 *} |
163 *} |
162 |
164 |
163 |
165 |
164 (** If-and-only-if rules **) |
166 (** If-and-only-if rules **) |
165 lemma iffR: |
167 lemma iffR: |