doc-src/IsarRef/Thy/document/HOL_Specific.tex

--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 29 11:35:47 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 29 11:49:56 2010 +0200
@@ -93,7 +93,7 @@
   \end{matharray}
 
   \begin{rail}
-    'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
+    'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
     ;
   \end{rail}
 
@@ -364,7 +364,7 @@
   \begin{rail}
     'datatype' (dtspec + 'and')
     ;
-    'rep\_datatype' ('(' (name +) ')')? (term +)
+    'rep_datatype' ('(' (name +) ')')? (term +)
     ;
 
     dtspec: parname? typespec mixfix? '=' (cons + '|')
@@ -511,9 +511,9 @@
   \begin{rail}
     'relation' term
     ;
-    'lexicographic\_order' ( clasimpmod * )
+    'lexicographic_order' ( clasimpmod * )
     ;
-    'size\_change' ( orders ( clasimpmod * ) )
+    'size_change' ( orders ( clasimpmod * ) )
     ;
     orders: ( 'max' | 'min' | 'ms' ) *
   \end{rail}
@@ -642,7 +642,7 @@
     ;
     hints: '(' 'hints' ( recdefmod * ) ')'
     ;
-    recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
+    recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
     ;
     tc: nameref ('(' nat ')')?
     ;
@@ -680,7 +680,7 @@
   \end{matharray}
 
   \begin{rail}
-    ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')
+    ('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del')
     ;
   \end{rail}%
 \end{isamarkuptext}%
@@ -722,7 +722,7 @@
   \end{matharray}
 
   \begin{rail}
-    ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
+    ('inductive' | 'inductive_set' | 'coinductive' | 'coinductive_set') target? fixes ('for' fixes)? \\
     ('where' clauses)? ('monos' thmrefs)?
     ;
     clauses: (thmdecl? prop + '|')
@@ -1010,13 +1010,13 @@
   \end{matharray}
 
   \begin{rail}
-    'case\_tac' goalspec? term rule?
+    'case_tac' goalspec? term rule?
     ;
-    'induct\_tac' goalspec? (insts * 'and') rule?
+    'induct_tac' goalspec? (insts * 'and') rule?
     ;
-    'ind\_cases' (prop +) ('for' (name +)) ?
+    'ind_cases' (prop +) ('for' (name +)) ?
     ;
-    'inductive\_cases' (thmdecl? (prop +) + 'and')
+    'inductive_cases' (thmdecl? (prop +) + 'and')
     ;
 
     rule: ('rule' ':' thmref)
@@ -1093,8 +1093,8 @@
   \end{matharray}
 
   \begin{rail}
-     'export\_code' ( constexpr + ) \\
-       ( ( 'in' target ( 'module\_name' string ) ? \\
+     'export_code' ( constexpr + ) \\
+       ( ( 'in' target ( 'module_name' string ) ? \\
         ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
     ;
 
@@ -1116,10 +1116,10 @@
     'code' ( 'del' | 'abstype' | 'abstract' ) ?
     ;
 
-    'code\_abort' ( const + )
+    'code_abort' ( const + )
     ;
 
-    'code\_datatype' ( const + )
+    'code_datatype' ( const + )
     ;
 
     'code_inline' ( 'del' ) ?
@@ -1128,41 +1128,41 @@
     'code_post' ( 'del' ) ?
     ;
 
-    'code\_thms' ( constexpr + ) ?
+    'code_thms' ( constexpr + ) ?
     ;
 
-    'code\_deps' ( constexpr + ) ?
+    'code_deps' ( constexpr + ) ?
     ;
 
-    'code\_const' (const + 'and') \\
+    'code_const' (const + 'and') \\
       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
     ;
 
-    'code\_type' (typeconstructor + 'and') \\
+    'code_type' (typeconstructor + 'and') \\
       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
     ;
 
-    'code\_class' (class + 'and') \\
+    'code_class' (class + 'and') \\
       ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
     ;
 
-    'code\_instance' (( typeconstructor '::' class ) + 'and') \\
+    'code_instance' (( typeconstructor '::' class ) + 'and') \\
       ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
     ;
 
-    'code\_reserved' target ( string + )
+    'code_reserved' target ( string + )
     ;
 
-    'code\_monad' const const target
+    'code_monad' const const target
     ;
 
-    'code\_include' target ( string ( string | '-') )
+    'code_include' target ( string ( string | '-') )
     ;
 
-    'code\_modulename' target ( ( string string ) + )
+    'code_modulename' target ( ( string string ) + )
     ;
 
-    'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
+    'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
       ( 'functions' ( string + ) ) ? ( 'file' string ) ?
     ;
 
@@ -1293,7 +1293,7 @@
   \end{matharray}
 
   \begin{rail}
-  ( 'code\_module' | 'code\_library' ) modespec ? name ? \\
+  ( 'code_module' | 'code_library' ) modespec ? name ? \\
     ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
     'contains' ( ( name '=' term ) + | term + )
   ;
@@ -1301,13 +1301,13 @@
   modespec: '(' ( name * ) ')'
   ;
 
-  'consts\_code' (codespec +)
+  'consts_code' (codespec +)
   ;
 
   codespec: const template attachment ?
   ;
 
-  'types\_code' (tycodespec +)
+  'types_code' (tycodespec +)
   ;
 
   tycodespec: name template attachment ?
@@ -1339,7 +1339,7 @@
   \end{matharray}
 
   \begin{rail}
-  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
+  ('specification' | 'ax_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
   ;
   decl: ((name ':')? term '(' 'overloaded' ')'?)
   \end{rail}