--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex Fri Oct 29 11:35:47 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex Fri Oct 29 11:49:56 2010 +0200
@@ -91,11 +91,11 @@
;
monos: ('monos' thmrefs)?
;
- condefs: ('con\_defs' thmrefs)?
+ condefs: ('con_defs' thmrefs)?
;
- typeintros: ('type\_intros' thmrefs)?
+ typeintros: ('type_intros' thmrefs)?
;
- typeelims: ('type\_elims' thmrefs)?
+ typeelims: ('type_elims' thmrefs)?
;
\end{rail}
@@ -153,7 +153,7 @@
\end{matharray}
\begin{rail}
- ('case\_tac' | 'induct\_tac') goalspec? name
+ ('case_tac' | 'induct_tac') goalspec? name
;
indcases (prop +)
;