doc-src/IsarRef/Thy/document/ZF_Specific.tex
changeset 40255 9ffbc25e1606
parent 30172 afdf7808cfd0
child 40406 313a24b66a8d
     1.1 --- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Fri Oct 29 11:35:47 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Fri Oct 29 11:49:56 2010 +0200
     1.3 @@ -91,11 +91,11 @@
     1.4      ;
     1.5      monos: ('monos' thmrefs)?
     1.6      ;
     1.7 -    condefs: ('con\_defs' thmrefs)?
     1.8 +    condefs: ('con_defs' thmrefs)?
     1.9      ;
    1.10 -    typeintros: ('type\_intros' thmrefs)?
    1.11 +    typeintros: ('type_intros' thmrefs)?
    1.12      ;
    1.13 -    typeelims: ('type\_elims' thmrefs)?
    1.14 +    typeelims: ('type_elims' thmrefs)?
    1.15      ;
    1.16    \end{rail}
    1.17  
    1.18 @@ -153,7 +153,7 @@
    1.19    \end{matharray}
    1.20  
    1.21    \begin{rail}
    1.22 -    ('case\_tac' | 'induct\_tac') goalspec? name
    1.23 +    ('case_tac' | 'induct_tac') goalspec? name
    1.24      ;
    1.25      indcases (prop +)
    1.26      ;