# HG changeset patch
# User wenzelm
# Date 1288366737 -7200
# Node ID 364aa76f7e21528c63a83317978074e7fb637e1f
# Parent  b12ae24459851ced225afbc228a0d5337b9b74a2# Parent  56e705fc8fdb1fcad95316685acd81bc63bb55a5
merged

diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Fri Oct 29 17:38:57 2010 +0200
@@ -201,7 +201,7 @@
   ;
   'sort' sort
   ;
-  ('type\_name' | 'type\_abbrev' | 'nonterminal') nameref
+  ('type_name' | 'type_abbrev' | 'nonterminal') nameref
   ;
   'typ' type
   ;
@@ -437,7 +437,7 @@
   \end{matharray}
 
   \begin{rail}
-  ('const\_name' | 'const\_abbrev') nameref
+  ('const_name' | 'const_abbrev') nameref
   ;
   'const' ('(' (type + ',') ')')?
   ;
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarImplementation/Thy/document/Logic.tex
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Fri Oct 29 17:38:57 2010 +0200
@@ -218,7 +218,7 @@
   ;
   'sort' sort
   ;
-  ('type\_name' | 'type\_abbrev' | 'nonterminal') nameref
+  ('type_name' | 'type_abbrev' | 'nonterminal') nameref
   ;
   'typ' type
   ;
@@ -464,7 +464,7 @@
   \end{matharray}
 
   \begin{rail}
-  ('const\_name' | 'const\_abbrev') nameref
+  ('const_name' | 'const_abbrev') nameref
   ;
   'const' ('(' (type + ',') ')')?
   ;
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/Document_Preparation.thy
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Oct 29 17:38:57 2010 +0200
@@ -84,7 +84,7 @@
   \begin{rail}
     ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
     ;
-    ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
+    ('header' | 'text_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt_raw') text
     ;
   \end{rail}
 
@@ -198,10 +198,10 @@
       'goals' options |
       'subgoals' options |
       'prf' options thmrefs |
-      'full\_prf' options thmrefs |
+      'full_prf' options thmrefs |
       'ML' options name |
-      'ML\_type' options name |
-      'ML\_struct' options name
+      'ML_type' options name |
+      'ML_struct' options name
     ;
     options: '[' (option * ',') ']'
     ;
@@ -468,7 +468,7 @@
   \end{matharray}
 
   \begin{rail}
-    ('display\_drafts' | 'print\_drafts') (name +)
+    ('display_drafts' | 'print_drafts') (name +)
     ;
   \end{rail}
 
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Fri Oct 29 17:38:57 2010 +0200
@@ -284,14 +284,14 @@
   \end{matharray}
 
   \begin{rail}
-    ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
+    ( 'rule_tac' | 'erule_tac' | 'drule_tac' | 'frule_tac' | 'cut_tac' | 'thin_tac' ) goalspec?
     ( insts thmref | thmrefs )
     ;
-    'subgoal\_tac' goalspec? (prop +)
+    'subgoal_tac' goalspec? (prop +)
     ;
-    'rename\_tac' goalspec? (name +)
+    'rename_tac' goalspec? (name +)
     ;
-    'rotate\_tac' goalspec? int?
+    'rotate_tac' goalspec? int?
     ;
     ('tactic' | 'raw_tactic') text
     ;
@@ -364,10 +364,10 @@
 
   \indexouternonterm{simpmod}
   \begin{rail}
-    ('simp' | 'simp\_all') opt? (simpmod *)
+    ('simp' | 'simp_all') opt? (simpmod *)
     ;
 
-    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
+    opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
     ;
     simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
       'split' (() | 'add' | 'del')) ':' thmrefs
@@ -471,7 +471,7 @@
   \end{matharray}
 
   \begin{rail}
-    'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
+    'simproc_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
     ;
 
     'simproc' (('add' ':')? | 'del' ':') (name+)
@@ -519,7 +519,7 @@
     'simplified' opt? thmrefs?
     ;
 
-    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
+    opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
     ;
   \end{rail}
 
@@ -785,7 +785,7 @@
     ;
     'atomize' ('(' 'full' ')')?
     ;
-    'rule\_format' ('(' 'noasm' ')')?
+    'rule_format' ('(' 'noasm' ')')?
     ;
   \end{rail}
 
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 29 17:38:57 2010 +0200
@@ -72,7 +72,7 @@
   \end{matharray}
 
   \begin{rail}
-    'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
+    'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
     ;
   \end{rail}
 
@@ -355,7 +355,7 @@
   \begin{rail}
     'datatype' (dtspec + 'and')
     ;
-    'rep\_datatype' ('(' (name +) ')')? (term +)
+    'rep_datatype' ('(' (name +) ')')? (term +)
     ;
 
     dtspec: parname? typespec mixfix? '=' (cons + '|')
@@ -501,9 +501,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}
@@ -633,7 +633,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 ')')?
     ;
@@ -672,7 +672,7 @@
   \end{matharray}
 
   \begin{rail}
-    ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')
+    ('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del')
     ;
   \end{rail}
 *}
@@ -712,7 +712,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 + '|')
@@ -941,28 +941,29 @@
 
     \begin{description}
 
-      \item[size] specifies the maximum size of the search space for
-        assignment values.
+    \item[@{text size}] specifies the maximum size of the search space
+    for assignment values.
 
-      \item[iterations] sets how many sets of assignments are
-        generated for each particular size.
+    \item[@{text iterations}] sets how many sets of assignments are
+    generated for each particular size.
 
-      \item[no\_assms] specifies whether assumptions in
-        structured proofs should be ignored.
+    \item[@{text no_assms}] specifies whether assumptions in
+    structured proofs should be ignored.
 
-      \item[timeout] sets the time limit in seconds.
+    \item[@{text timeout}] sets the time limit in seconds.
 
-      \item[default\_type] sets the type(s) generally used to instantiate
-        type variables.
+    \item[@{text default_type}] sets the type(s) generally used to
+    instantiate type variables.
 
-      \item[report] if set quickcheck reports how many tests fulfilled
-        the preconditions.
+    \item[@{text report}] if set quickcheck reports how many tests
+    fulfilled the preconditions.
 
-      \item[quiet] if not set quickcheck informs about the current size
-        for assignment values.
+    \item[@{text quiet}] if not set quickcheck informs about the
+    current size for assignment values.
 
-      \item[expect] can be used to check if the user's expectation was met
-        (no\_expectation, no\_counterexample, or counterexample)
+    \item[@{text expect}] can be used to check if the user's
+    expectation was met (@{text no_expectation}, @{text
+    no_counterexample}, or @{text counterexample}).
 
     \end{description}
 
@@ -990,13 +991,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)
@@ -1077,8 +1078,8 @@
   \end{matharray}
 
   \begin{rail}
-     'export\_code' ( constexpr + ) \\
-       ( ( 'in' target ( 'module\_name' string ) ? \\
+     'export_code' ( constexpr + ) \\
+       ( ( 'in' target ( 'module_name' string ) ? \\
         ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
     ;
 
@@ -1100,10 +1101,10 @@
     'code' ( 'del' | 'abstype' | 'abstract' ) ?
     ;
 
-    'code\_abort' ( const + )
+    'code_abort' ( const + )
     ;
 
-    'code\_datatype' ( const + )
+    'code_datatype' ( const + )
     ;
 
     'code_inline' ( 'del' ) ?
@@ -1112,41 +1113,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 ) ?
     ;
 
@@ -1280,7 +1281,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 + )
   ;
@@ -1288,13 +1289,13 @@
   modespec: '(' ( name * ) ')'
   ;
 
-  'consts\_code' (codespec +)
+  'consts_code' (codespec +)
   ;
 
   codespec: const template attachment ?
   ;
 
-  'types\_code' (tycodespec +)
+  'types_code' (tycodespec +)
   ;
 
   tycodespec: name template attachment ?
@@ -1325,7 +1326,7 @@
   \end{matharray}
 
   \begin{rail}
-  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
+  ('specification' | 'ax_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
   ;
   decl: ((name ':')? term '(' 'overloaded' ')'?)
   \end{rail}
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Oct 29 17:38:57 2010 +0200
@@ -31,7 +31,7 @@
     ;
     'thm' modes? thmrefs
     ;
-    ( 'prf' | 'full\_prf' ) modes? thmrefs?
+    ( 'prf' | 'full_prf' ) modes? thmrefs?
     ;
     'pr' modes? nat?
     ;
@@ -364,9 +364,9 @@
   \end{matharray}
 
   \begin{rail}
-    ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
+    ('type_notation' | 'no_type_notation') target? mode? \\ (nameref mixfix + 'and')
     ;
-    ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
+    ('notation' | 'no_notation') target? mode? \\ (nameref structmixfix + 'and')
     ;
     'write' mode? (nameref structmixfix + 'and')
     ;
@@ -730,9 +730,9 @@
   \begin{rail}
     'nonterminals' (name +)
     ;
-    ('syntax' | 'no\_syntax') mode? (constdecl +)
+    ('syntax' | 'no_syntax') mode? (constdecl +)
     ;
-    ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
+    ('translations' | 'no_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
     ;
 
     mode: ('(' ( name | 'output' | name 'output' ) ')')
@@ -786,8 +786,8 @@
   \end{matharray}
 
   \begin{rail}
-  ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
-    'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
+  ( 'parse_ast_translation' | 'parse_translation' | 'print_translation' |
+    'typed_print_translation' | 'print_ast_translation' ) ('(advanced)')? text
   ;
   \end{rail}
 
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/Misc.thy
--- a/doc-src/IsarRef/Thy/Misc.thy	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/Misc.thy	Fri Oct 29 17:38:57 2010 +0200
@@ -21,19 +21,19 @@
   \end{matharray}
 
   \begin{rail}
-    ('print\_theory' | 'print\_theorems') ('!'?)
+    ('print_theory' | 'print_theorems') ('!'?)
     ;
 
-    'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
+    'find_theorems' (('(' (nat)? ('with_dups')? ')')?) (thmcriterion *)
     ;
     thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
       'solves' | 'simp' ':' term | term)
     ;
-    'find\_consts' (constcriterion *)
+    'find_consts' (constcriterion *)
     ;
     constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
     ;
-    'thm\_deps' thmrefs
+    'thm_deps' thmrefs
     ;
   \end{rail}
 
@@ -143,7 +143,7 @@
   \end{matharray}
 
   \begin{rail}
-    ('cd' | 'use\_thy') name
+    ('cd' | 'use_thy') name
     ;
   \end{rail}
 
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Fri Oct 29 17:38:57 2010 +0200
@@ -432,11 +432,11 @@
 
   \begin{rail}
     ('lemma' | 'theorem' | 'corollary' |
-     'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal)
+     'schematic_lemma' | 'schematic_theorem' | 'schematic_corollary') target? (goal | longgoal)
     ;
     ('have' | 'show' | 'hence' | 'thus') goal
     ;
-    'print\_statement' modes? thmrefs
+    'print_statement' modes? thmrefs
     ;
   
     goal: (props + 'and')
@@ -834,7 +834,7 @@
   \end{matharray}
 
   \begin{rail}
-    ( 'apply' | 'apply\_end' ) method
+    ( 'apply' | 'apply_end' ) method
     ;
     'defer' nat?
     ;
@@ -896,7 +896,7 @@
   \end{matharray}
 
   \begin{rail}
-    'method\_setup' name '=' text text
+    'method_setup' name '=' text text
     ;
   \end{rail}
 
@@ -1190,9 +1190,9 @@
     caseref: nameref attributes?
     ;
 
-    'case\_names' (name +)
+    'case_names' (name +)
     ;
-    'case\_conclusion' name (name *)
+    'case_conclusion' name (name *)
     ;
     'params' ((name *) + 'and')
     ;
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Oct 29 17:38:57 2010 +0200
@@ -322,8 +322,8 @@
   A locale instance consists of a reference to a locale and either
   positional or named parameter instantiations.  Identical
   instantiations (that is, those that instante a parameter by itself)
-  may be omitted.  The notation `\_' enables to omit the instantiation
-  for a parameter inside a positional instantiation.
+  may be omitted.  The notation `@{text "_"}' enables to omit the
+  instantiation for a parameter inside a positional instantiation.
 
   Terms in instantiations are from the context the locale expressions
   is declared in.  Local names may be added to this context with the
@@ -360,7 +360,7 @@
   \begin{rail}
     'locale' name ('=' locale)? 'begin'?
     ;
-    'print\_locale' '!'? nameref
+    'print_locale' '!'? nameref
     ;
     locale: contextelem+ | localeexpr ('+' (contextelem+))?
     ;
@@ -503,7 +503,7 @@
     ;
     'interpret' localeexpr equations?
     ;
-    'print\_interps' nameref
+    'print_interps' nameref
     ;
     equations: 'where' (thmdecl? prop + 'and')
     ;
@@ -630,9 +630,9 @@
     ;
     'instance' nameref ('<' | subseteq) nameref
     ;
-    'print\_classes'
+    'print_classes'
     ;
-    'class\_deps'
+    'class_deps'
     ;
 
     superclassexpr: nameref | (nameref '+' superclassexpr)
@@ -840,9 +840,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}
 
@@ -930,7 +930,7 @@
     ;
     'classrel' (nameref ('<' | subseteq) nameref + 'and')
     ;
-    'default\_sort' sort
+    'default_sort' sort
     ;
   \end{rail}
 
@@ -1176,7 +1176,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}
 
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/ZF_Specific.thy
--- a/doc-src/IsarRef/Thy/ZF_Specific.thy	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/ZF_Specific.thy	Fri Oct 29 17:38:57 2010 +0200
@@ -67,11 +67,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}
 
@@ -126,7 +126,7 @@
   \end{matharray}
 
   \begin{rail}
-    ('case\_tac' | 'induct\_tac') goalspec? name
+    ('case_tac' | 'induct_tac') goalspec? name
     ;
     indcases (prop +)
     ;
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Oct 29 17:38:57 2010 +0200
@@ -105,7 +105,7 @@
   \begin{rail}
     ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
     ;
-    ('header' | 'text\_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
+    ('header' | 'text_raw' | 'sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt_raw') text
     ;
   \end{rail}
 
@@ -216,10 +216,10 @@
       'goals' options |
       'subgoals' options |
       'prf' options thmrefs |
-      'full\_prf' options thmrefs |
+      'full_prf' options thmrefs |
       'ML' options name |
-      'ML\_type' options name |
-      'ML\_struct' options name
+      'ML_type' options name |
+      'ML_struct' options name
     ;
     options: '[' (option * ',') ']'
     ;
@@ -487,7 +487,7 @@
   \end{matharray}
 
   \begin{rail}
-    ('display\_drafts' | 'print\_drafts') (name +)
+    ('display_drafts' | 'print_drafts') (name +)
     ;
   \end{rail}
 
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Fri Oct 29 17:38:57 2010 +0200
@@ -302,14 +302,14 @@
   \end{matharray}
 
   \begin{rail}
-    ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec?
+    ( 'rule_tac' | 'erule_tac' | 'drule_tac' | 'frule_tac' | 'cut_tac' | 'thin_tac' ) goalspec?
     ( insts thmref | thmrefs )
     ;
-    'subgoal\_tac' goalspec? (prop +)
+    'subgoal_tac' goalspec? (prop +)
     ;
-    'rename\_tac' goalspec? (name +)
+    'rename_tac' goalspec? (name +)
     ;
-    'rotate\_tac' goalspec? int?
+    'rotate_tac' goalspec? int?
     ;
     ('tactic' | 'raw_tactic') text
     ;
@@ -384,10 +384,10 @@
 
   \indexouternonterm{simpmod}
   \begin{rail}
-    ('simp' | 'simp\_all') opt? (simpmod *)
+    ('simp' | 'simp_all') opt? (simpmod *)
     ;
 
-    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
+    opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
     ;
     simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
       'split' (() | 'add' | 'del')) ':' thmrefs
@@ -490,7 +490,7 @@
   \end{matharray}
 
   \begin{rail}
-    'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
+    'simproc_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))?
     ;
 
     'simproc' (('add' ':')? | 'del' ':') (name+)
@@ -538,7 +538,7 @@
     'simplified' opt? thmrefs?
     ;
 
-    opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')'
+    opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
     ;
   \end{rail}
 
@@ -809,7 +809,7 @@
     ;
     'atomize' ('(' 'full' ')')?
     ;
-    'rule\_format' ('(' 'noasm' ')')?
+    'rule_format' ('(' 'noasm' ')')?
     ;
   \end{rail}
 
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 29 17:38:57 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 + '|')
@@ -959,14 +959,28 @@
 
     \begin{description}
 
-      \item[size] specifies the maximum size of the search space for
-        assignment values.
+    \item[\isa{size}] specifies the maximum size of the search space
+    for assignment values.
+
+    \item[\isa{iterations}] sets how many sets of assignments are
+    generated for each particular size.
+
+    \item[\isa{no{\isacharunderscore}assms}] specifies whether assumptions in
+    structured proofs should be ignored.
+
+    \item[\isa{timeout}] sets the time limit in seconds.
 
-      \item[iterations] sets how many sets of assignments are
-        generated for each particular size.
+    \item[\isa{default{\isacharunderscore}type}] sets the type(s) generally used to
+    instantiate type variables.
+
+    \item[\isa{report}] if set quickcheck reports how many tests
+    fulfilled the preconditions.
 
-      \item[no\_assms] specifies whether assumptions in
-        structured proofs should be ignored.
+    \item[\isa{quiet}] if not set quickcheck informs about the
+    current size for assignment values.
+
+    \item[\isa{expect}] can be used to check if the user's
+    expectation was met (\isa{no{\isacharunderscore}expectation}, \isa{no{\isacharunderscore}counterexample}, or \isa{counterexample}).
 
     \end{description}
 
@@ -996,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)
@@ -1079,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 ')' ) ?) + ) ?
     ;
 
@@ -1102,10 +1116,10 @@
     'code' ( 'del' | 'abstype' | 'abstract' ) ?
     ;
 
-    'code\_abort' ( const + )
+    'code_abort' ( const + )
     ;
 
-    'code\_datatype' ( const + )
+    'code_datatype' ( const + )
     ;
 
     'code_inline' ( 'del' ) ?
@@ -1114,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 ) ?
     ;
 
@@ -1279,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 + )
   ;
@@ -1287,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 ?
@@ -1325,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}
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Fri Oct 29 17:38:57 2010 +0200
@@ -53,7 +53,7 @@
     ;
     'thm' modes? thmrefs
     ;
-    ( 'prf' | 'full\_prf' ) modes? thmrefs?
+    ( 'prf' | 'full_prf' ) modes? thmrefs?
     ;
     'pr' modes? nat?
     ;
@@ -387,9 +387,9 @@
   \end{matharray}
 
   \begin{rail}
-    ('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and')
+    ('type_notation' | 'no_type_notation') target? mode? \\ (nameref mixfix + 'and')
     ;
-    ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
+    ('notation' | 'no_notation') target? mode? \\ (nameref structmixfix + 'and')
     ;
     'write' mode? (nameref structmixfix + 'and')
     ;
@@ -749,9 +749,9 @@
   \begin{rail}
     'nonterminals' (name +)
     ;
-    ('syntax' | 'no\_syntax') mode? (constdecl +)
+    ('syntax' | 'no_syntax') mode? (constdecl +)
     ;
-    ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
+    ('translations' | 'no_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
     ;
 
     mode: ('(' ( name | 'output' | name 'output' ) ')')
@@ -806,8 +806,8 @@
   \end{matharray}
 
   \begin{rail}
-  ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
-    'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
+  ( 'parse_ast_translation' | 'parse_translation' | 'print_translation' |
+    'typed_print_translation' | 'print_ast_translation' ) ('(advanced)')? text
   ;
   \end{rail}
 
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/document/Misc.tex
--- a/doc-src/IsarRef/Thy/document/Misc.tex	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Misc.tex	Fri Oct 29 17:38:57 2010 +0200
@@ -41,19 +41,19 @@
   \end{matharray}
 
   \begin{rail}
-    ('print\_theory' | 'print\_theorems') ('!'?)
+    ('print_theory' | 'print_theorems') ('!'?)
     ;
 
-    'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *)
+    'find_theorems' (('(' (nat)? ('with_dups')? ')')?) (thmcriterion *)
     ;
     thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
       'solves' | 'simp' ':' term | term)
     ;
-    'find\_consts' (constcriterion *)
+    'find_consts' (constcriterion *)
     ;
     constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
     ;
-    'thm\_deps' thmrefs
+    'thm_deps' thmrefs
     ;
   \end{rail}
 
@@ -164,7 +164,7 @@
   \end{matharray}
 
   \begin{rail}
-    ('cd' | 'use\_thy') name
+    ('cd' | 'use_thy') name
     ;
   \end{rail}
 
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Fri Oct 29 17:38:57 2010 +0200
@@ -453,11 +453,11 @@
 
   \begin{rail}
     ('lemma' | 'theorem' | 'corollary' |
-     'schematic\_lemma' | 'schematic\_theorem' | 'schematic\_corollary') target? (goal | longgoal)
+     'schematic_lemma' | 'schematic_theorem' | 'schematic_corollary') target? (goal | longgoal)
     ;
     ('have' | 'show' | 'hence' | 'thus') goal
     ;
-    'print\_statement' modes? thmrefs
+    'print_statement' modes? thmrefs
     ;
   
     goal: (props + 'and')
@@ -843,7 +843,7 @@
   \end{matharray}
 
   \begin{rail}
-    ( 'apply' | 'apply\_end' ) method
+    ( 'apply' | 'apply_end' ) method
     ;
     'defer' nat?
     ;
@@ -903,7 +903,7 @@
   \end{matharray}
 
   \begin{rail}
-    'method\_setup' name '=' text text
+    'method_setup' name '=' text text
     ;
   \end{rail}
 
@@ -1192,9 +1192,9 @@
     caseref: nameref attributes?
     ;
 
-    'case\_names' (name +)
+    'case_names' (name +)
     ;
-    'case\_conclusion' name (name *)
+    'case_conclusion' name (name *)
     ;
     'params' ((name *) + 'and')
     ;
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 29 17:38:57 2010 +0200
@@ -346,8 +346,8 @@
   A locale instance consists of a reference to a locale and either
   positional or named parameter instantiations.  Identical
   instantiations (that is, those that instante a parameter by itself)
-  may be omitted.  The notation `\_' enables to omit the instantiation
-  for a parameter inside a positional instantiation.
+  may be omitted.  The notation `\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}' enables to omit the
+  instantiation for a parameter inside a positional instantiation.
 
   Terms in instantiations are from the context the locale expressions
   is declared in.  Local names may be added to this context with the
@@ -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}
 
diff -r b12ae2445985 -r 364aa76f7e21 doc-src/IsarRef/Thy/document/ZF_Specific.tex
--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Fri Oct 29 17:28:27 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Fri Oct 29 17:38:57 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 +)
     ;