1.1 --- a/doc-src/IsarRef/Thy/Generic.thy Tue Jun 17 04:19:50 2008 +0200
1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy Wed Jun 18 16:55:21 2008 +0200
1.3 @@ -318,7 +318,7 @@
1.4 assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
1.5 \cite[\S3]{isabelle-ref}. Note that the scope of schematic
1.6 variables is spread over the main goal statement. Instantiations
1.7 - may be given as well, see also ML tactic @{ML Tactic.cut_inst_tac}
1.8 + may be given as well, see also ML tactic @{ML cut_inst_tac}
1.9 in \cite[\S3]{isabelle-ref}.
1.10
1.11 \item [@{method thin_tac}~@{text \<phi>}] deletes the specified