changeset 42705 | 528a2ba8fa74 |
parent 42704 | 3f19e324ff59 |
--- a/doc-src/IsarRef/Thy/ZF_Specific.thy Thu May 05 23:15:11 2011 +0200 +++ b/doc-src/IsarRef/Thy/ZF_Specific.thy Thu May 05 23:23:02 2011 +0200 @@ -123,7 +123,7 @@ \end{matharray} @{rail " - (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goalspec}? @{syntax name} + (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name} ; @@{method (ZF) ind_cases} (@{syntax prop} +) ;