1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 29 11:35:47 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 29 11:49:56 2010 +0200
     1.3 @@ -385,7 +385,7 @@
     1.4    \begin{rail}
     1.5      'locale' name ('=' locale)? 'begin'?
     1.6      ;
     1.7 -    'print\_locale' '!'? nameref
     1.8 +    'print_locale' '!'? nameref
     1.9      ;
    1.10      locale: contextelem+ | localeexpr ('+' (contextelem+))?
    1.11      ;
    1.12 @@ -525,7 +525,7 @@
    1.13      ;
    1.14      'interpret' localeexpr equations?
    1.15      ;
    1.16 -    'print\_interps' nameref
    1.17 +    'print_interps' nameref
    1.18      ;
    1.19      equations: 'where' (thmdecl? prop + 'and')
    1.20      ;
    1.21 @@ -653,9 +653,9 @@
    1.22      ;
    1.23      'instance' nameref ('<' | subseteq) nameref
    1.24      ;
    1.25 -    'print\_classes'
    1.26 +    'print_classes'
    1.27      ;
    1.28 -    'class\_deps'
    1.29 +    'class_deps'
    1.30      ;
    1.31  
    1.32      superclassexpr: nameref | (nameref '+' superclassexpr)
    1.33 @@ -862,9 +862,9 @@
    1.34    \begin{rail}
    1.35      'use' name
    1.36      ;
    1.37 -    ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
    1.38 +    ('ML' | 'ML_prf' | 'ML_val' | 'ML_command' | 'setup' | 'local_setup') text
    1.39      ;
    1.40 -    'attribute\_setup' name '=' text text
    1.41 +    'attribute_setup' name '=' text text
    1.42      ;
    1.43    \end{rail}
    1.44  
    1.45 @@ -966,7 +966,7 @@
    1.46      ;
    1.47      'classrel' (nameref ('<' | subseteq) nameref + 'and')
    1.48      ;
    1.49 -    'default\_sort' sort
    1.50 +    'default_sort' sort
    1.51      ;
    1.52    \end{rail}
    1.53  
    1.54 @@ -1218,7 +1218,7 @@
    1.55    \end{matharray}
    1.56  
    1.57    \begin{rail}
    1.58 -    ( 'hide\_class' | 'hide\_type' | 'hide\_const' | 'hide\_fact' ) ('(open)')? (nameref + )
    1.59 +    ( 'hide_class' | 'hide_type' | 'hide_const' | 'hide_fact' ) ('(open)')? (nameref + )
    1.60      ;
    1.61    \end{rail}
    1.62