equal
deleted
inserted
replaced
316 |
316 |
317 \item [@{method cut_tac}] inserts facts into the proof state as |
317 \item [@{method cut_tac}] inserts facts into the proof state as |
318 assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in |
318 assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in |
319 \cite[\S3]{isabelle-ref}. Note that the scope of schematic |
319 \cite[\S3]{isabelle-ref}. Note that the scope of schematic |
320 variables is spread over the main goal statement. Instantiations |
320 variables is spread over the main goal statement. Instantiations |
321 may be given as well, see also ML tactic @{ML Tactic.cut_inst_tac} |
321 may be given as well, see also ML tactic @{ML cut_inst_tac} |
322 in \cite[\S3]{isabelle-ref}. |
322 in \cite[\S3]{isabelle-ref}. |
323 |
323 |
324 \item [@{method thin_tac}~@{text \<phi>}] deletes the specified |
324 \item [@{method thin_tac}~@{text \<phi>}] deletes the specified |
325 assumption from a subgoal; note that @{text \<phi>} may contain schematic |
325 assumption from a subgoal; note that @{text \<phi>} may contain schematic |
326 variables. See also @{ML thin_tac} in |
326 variables. See also @{ML thin_tac} in |