--- a/doc-src/IsarRef/Thy/document/Spec.tex Fri Oct 29 11:35:47 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Fri Oct 29 11:49:56 2010 +0200
@@ -385,7 +385,7 @@
\begin{rail}
'locale' name ('=' locale)? 'begin'?
;
- 'print\_locale' '!'? nameref
+ 'print_locale' '!'? nameref
;
locale: contextelem+ | localeexpr ('+' (contextelem+))?
;
@@ -525,7 +525,7 @@
;
'interpret' localeexpr equations?
;
- 'print\_interps' nameref
+ 'print_interps' nameref
;
equations: 'where' (thmdecl? prop + 'and')
;
@@ -653,9 +653,9 @@
;
'instance' nameref ('<' | subseteq) nameref
;
- 'print\_classes'
+ 'print_classes'
;
- 'class\_deps'
+ 'class_deps'
;
superclassexpr: nameref | (nameref '+' superclassexpr)
@@ -862,9 +862,9 @@
\begin{rail}
'use' name
;
- ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
+ ('ML' | 'ML_prf' | 'ML_val' | 'ML_command' | 'setup' | 'local_setup') text
;
- 'attribute\_setup' name '=' text text
+ 'attribute_setup' name '=' text text
;
\end{rail}
@@ -966,7 +966,7 @@
;
'classrel' (nameref ('<' | subseteq) nameref + 'and')
;
- 'default\_sort' sort
+ 'default_sort' sort
;
\end{rail}
@@ -1218,7 +1218,7 @@
\end{matharray}
\begin{rail}
- ( 'hide\_class' | 'hide\_type' | 'hide\_const' | 'hide\_fact' ) ('(open)')? (nameref + )
+ ( 'hide_class' | 'hide_type' | 'hide_const' | 'hide_fact' ) ('(open)')? (nameref + )
;
\end{rail}