pervasive cut_inst_tac;
authorwenzelm
Wed, 18 Jun 2008 16:55:21 +0200
changeset 272483c17b824650b
parent 27247 e5787c5be196
child 27249 f339dc43ce9f
pervasive cut_inst_tac;
doc-src/IsarRef/Thy/Generic.thy
     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