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