tuned some syntax names;

--- a/doc-src/IsarRef/Thy/Generic.thy	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Thu May 05 23:23:02 2011 +0200
@@ -292,14 +292,14 @@
 
   @{rail "
     (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
-      @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goalspec}? \\
+      @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \\
     ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
     ;
-    @@{method subgoal_tac} @{syntax goalspec}? (@{syntax prop} +)
+    @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)
     ;
-    @@{method rename_tac} @{syntax goalspec}? (@{syntax name} +)
+    @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
     ;
-    @@{method rotate_tac} @{syntax goalspec}? @{syntax int}?
+    @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
     ;
     (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
     ;

--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 05 23:23:02 2011 +0200
@@ -17,7 +17,7 @@
 
     altname: '(' (@{syntax name} | @'open' | @'open' @{syntax name}) ')'
     ;
-    abstype: @{syntax typespecsorts} @{syntax mixfix}?
+    abstype: @{syntax typespec_sorts} @{syntax mixfix}?
     ;
     repset: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})?
   "}
@@ -172,7 +172,7 @@
   \end{matharray}
 
   @{rail "
-    @@{command (HOL) record} @{syntax typespecsorts} '=' \\
+    @@{command (HOL) record} @{syntax typespec_sorts} '=' \\
       (@{syntax type} '+')? (@{syntax constdecl} +)
   "}
 
@@ -1136,9 +1136,9 @@
   \end{matharray}
 
   @{rail "
-    @@{method (HOL) case_tac} @{syntax goalspec}? @{syntax term} rule?
+    @@{method (HOL) case_tac} @{syntax goal_spec}? @{syntax term} rule?
     ;
-    @@{method (HOL) induct_tac} @{syntax goalspec}? (@{syntax insts} * @'and') rule?
+    @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?
     ;
     @@{method (HOL) ind_cases} (@{syntax prop}+) (@'for' (@{syntax name}+))?
     ;

--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu May 05 23:23:02 2011 +0200
@@ -248,7 +248,7 @@
     @{syntax_def mixfix}: @{syntax \"infix\"} | '(' @{syntax string} prios? @{syntax nat}? ')' |
     '(' @'binder' @{syntax string} prios? @{syntax nat} ')'
     ;
-    @{syntax_def structmixfix}: @{syntax mixfix} | '(' @'structure' ')'
+    @{syntax_def struct_mixfix}: @{syntax mixfix} | '(' @'structure' ')'
     ;
 
     prios: '[' (@{syntax nat} + ',') ']'
@@ -366,9 +366,9 @@
       @{syntax mode}? \\ (@{syntax nameref} @{syntax mixfix} + @'and')
     ;
     (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \\
-      (@{syntax nameref} @{syntax structmixfix} + @'and')
+      (@{syntax nameref} @{syntax struct_mixfix} + @'and')
     ;
-    @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax structmixfix} + @'and')
+    @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax struct_mixfix} + @'and')
   "}
 
   \begin{description}

--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu May 05 23:23:02 2011 +0200
@@ -304,7 +304,7 @@
     @{syntax_def typespec}:
       (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name}
     ;
-    @{syntax_def typespecsorts}:
+    @{syntax_def typespec_sorts}:
       (() | (@{syntax typefree} ('::' @{syntax sort})?) |
         '(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
   "}
@@ -319,9 +319,9 @@
   This works both for @{syntax term} and @{syntax prop}.
 
   @{rail "
-    @{syntax_def termpat}: '(' (@'is' @{syntax term} +) ')'
+    @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')'
     ;
-    @{syntax_def proppat}: '(' (@'is' @{syntax prop} +) ')'
+    @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')'
   "}
 
   \medskip Declarations of local variables @{text "x :: \<tau>"} and
@@ -335,7 +335,7 @@
   @{rail "
     @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
     ;
-    @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax proppat}? +)
+    @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
   "}
 
   The treatment of multiple declarations corresponds to the

--- a/doc-src/IsarRef/Thy/Proof.thy	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Thu May 05 23:23:02 2011 +0200
@@ -194,7 +194,7 @@
     ;
     @@{command def} (def + @'and')
     ;
-    def: @{syntax thmdecl}? \\ @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax termpat}?
+    def: @{syntax thmdecl}? \\ @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
   "}
 
   \begin{description}
@@ -269,8 +269,8 @@
     @@{command let} ((@{syntax term} + @'and') '=' @{syntax term} + @'and')
   "}
 
-  The syntax of @{keyword "is"} patterns follows @{syntax termpat} or
-  @{syntax proppat} (see \secref{sec:term-decls}).
+  The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or
+  @{syntax prop_pat} (see \secref{sec:term-decls}).
 
   \begin{description}
 
@@ -568,7 +568,7 @@
   "n"}.
 
   @{rail "
-    @{syntax_def goalspec}:
+    @{syntax_def goal_spec}:
       '[' (@{syntax nat} '-' @{syntax nat} | @{syntax nat} '-' | @{syntax nat} | '!' ) ']'
   "}
 *}

--- a/doc-src/IsarRef/Thy/Spec.thy	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Thu May 05 23:23:02 2011 +0200
@@ -371,7 +371,7 @@
       @'fixes' (@{syntax \"fixes\"} + @'and') |
       @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
       @'assumes' (@{syntax props} + @'and') |
-      @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax proppat}? + @'and') |
+      @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
       @'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and')
   "}
 

--- a/doc-src/IsarRef/Thy/ZF_Specific.thy	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/ZF_Specific.thy	Thu May 05 23:23:02 2011 +0200
@@ -123,7 +123,7 @@
   \end{matharray}
 
   @{rail "
-    (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goalspec}? @{syntax name}
+    (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name}
     ;
     @@{method (ZF) ind_cases} (@{syntax prop} +)
     ;

--- a/doc-src/IsarRef/Thy/document/Generic.tex	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Thu May 05 23:23:02 2011 +0200
@@ -443,7 +443,7 @@
 \rail@endbar
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
+\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
 \rail@endbar
 \rail@cr{7}
 \rail@bar
@@ -458,7 +458,7 @@
 \rail@term{\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
+\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
 \rail@endbar
 \rail@plus
 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
@@ -469,7 +469,7 @@
 \rail@term{\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
+\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
 \rail@endbar
 \rail@plus
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
@@ -480,7 +480,7 @@
 \rail@term{\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
+\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
 \rail@endbar
 \rail@bar
 \rail@nextbar{1}

--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 05 23:23:02 2011 +0200
@@ -55,7 +55,7 @@
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@end
 \rail@begin{2}{\isa{abstype}}
-\rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
+\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
@@ -239,7 +239,7 @@
   \begin{railoutput}
 \rail@begin{4}{}
 \rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
-\rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
+\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
 \rail@cr{2}
 \rail@bar
@@ -1604,7 +1604,7 @@
 \rail@term{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
+\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
 \rail@endbar
 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
 \rail@bar
@@ -1616,7 +1616,7 @@
 \rail@term{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
+\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
 \rail@endbar
 \rail@bar
 \rail@nextbar{1}

--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu May 05 23:23:02 2011 +0200
@@ -358,7 +358,7 @@
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{\indexdef{}{syntax}{structmixfix}\hypertarget{syntax.structmixfix}{\hyperlink{syntax.structmixfix}{\mbox{\isa{structmixfix}}}}}
+\rail@begin{2}{\indexdef{}{syntax}{struct\_mixfix}\hypertarget{syntax.struct-mixfix}{\hyperlink{syntax.struct-mixfix}{\mbox{\isa{struct{\isaliteral{5F}{\isacharunderscore}}mixfix}}}}}
 \rail@bar
 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
 \rail@nextbar{1}
@@ -527,7 +527,7 @@
 \rail@cr{3}
 \rail@plus
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
-\rail@nont{\hyperlink{syntax.structmixfix}{\mbox{\isa{structmixfix}}}}[]
+\rail@nont{\hyperlink{syntax.struct-mixfix}{\mbox{\isa{struct{\isaliteral{5F}{\isacharunderscore}}mixfix}}}}[]
 \rail@nextplus{4}
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus
@@ -540,7 +540,7 @@
 \rail@endbar
 \rail@plus
 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
-\rail@nont{\hyperlink{syntax.structmixfix}{\mbox{\isa{structmixfix}}}}[]
+\rail@nont{\hyperlink{syntax.struct-mixfix}{\mbox{\isa{struct{\isaliteral{5F}{\isacharunderscore}}mixfix}}}}[]
 \rail@nextplus{1}
 \rail@cterm{\isa{\isakeyword{and}}}[]
 \rail@endplus

--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Thu May 05 23:23:02 2011 +0200
@@ -432,7 +432,7 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@end
-\rail@begin{6}{\indexdef{}{syntax}{typespecsorts}\hypertarget{syntax.typespecsorts}{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}}
+\rail@begin{6}{\indexdef{}{syntax}{typespec\_sorts}\hypertarget{syntax.typespec-sorts}{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}}
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}}}[]
@@ -472,7 +472,7 @@
   This works both for \hyperlink{syntax.term}{\mbox{\isa{term}}} and \hyperlink{syntax.prop}{\mbox{\isa{prop}}}.
 
   \begin{railoutput}
-\rail@begin{2}{\indexdef{}{syntax}{termpat}\hypertarget{syntax.termpat}{\hyperlink{syntax.termpat}{\mbox{\isa{termpat}}}}}
+\rail@begin{2}{\indexdef{}{syntax}{term\_pat}\hypertarget{syntax.term-pat}{\hyperlink{syntax.term-pat}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}pat}}}}}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
 \rail@plus
 \rail@term{\isa{\isakeyword{is}}}[]
@@ -481,7 +481,7 @@
 \rail@endplus
 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
 \rail@end
-\rail@begin{2}{\indexdef{}{syntax}{proppat}\hypertarget{syntax.proppat}{\hyperlink{syntax.proppat}{\mbox{\isa{proppat}}}}}
+\rail@begin{2}{\indexdef{}{syntax}{prop\_pat}\hypertarget{syntax.prop-pat}{\hyperlink{syntax.prop-pat}{\mbox{\isa{prop{\isaliteral{5F}{\isacharunderscore}}pat}}}}}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
 \rail@plus
 \rail@term{\isa{\isakeyword{is}}}[]
@@ -522,7 +522,7 @@
 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.proppat}{\mbox{\isa{proppat}}}}[]
+\rail@nont{\hyperlink{syntax.prop-pat}{\mbox{\isa{prop{\isaliteral{5F}{\isacharunderscore}}pat}}}}[]
 \rail@endbar
 \rail@nextplus{2}
 \rail@endplus

--- a/doc-src/IsarRef/Thy/document/Proof.tex	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Thu May 05 23:23:02 2011 +0200
@@ -263,7 +263,7 @@
 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
 \rail@bar
 \rail@nextbar{4}
-\rail@nont{\hyperlink{syntax.termpat}{\mbox{\isa{termpat}}}}[]
+\rail@nont{\hyperlink{syntax.term-pat}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}pat}}}}[]
 \rail@endbar
 \rail@end
 \end{railoutput}
@@ -348,8 +348,8 @@
 \end{railoutput}
 
 
-  The syntax of \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns follows \hyperlink{syntax.termpat}{\mbox{\isa{termpat}}} or
-  \hyperlink{syntax.proppat}{\mbox{\isa{proppat}}} (see \secref{sec:term-decls}).
+  The syntax of \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns follows \hyperlink{syntax.term-pat}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}pat}}} or
+  \hyperlink{syntax.prop-pat}{\mbox{\isa{prop{\isaliteral{5F}{\isacharunderscore}}pat}}} (see \secref{sec:term-decls}).
 
   \begin{description}
 
@@ -780,7 +780,7 @@
   all goals, and ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{2D}{\isacharminus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}'' to all goals starting from \isa{{\isaliteral{22}{\isachardoublequote}}n{\isaliteral{22}{\isachardoublequote}}}.
 
   \begin{railoutput}
-\rail@begin{4}{\indexdef{}{syntax}{goalspec}\hypertarget{syntax.goalspec}{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}}
+\rail@begin{4}{\indexdef{}{syntax}{goal\_spec}\hypertarget{syntax.goal-spec}{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}}
 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
 \rail@bar
 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]

--- a/doc-src/IsarRef/Thy/document/Spec.tex	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Thu May 05 23:23:02 2011 +0200
@@ -645,7 +645,7 @@
 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
 \rail@bar
 \rail@nextbar{7}
-\rail@nont{\hyperlink{syntax.proppat}{\mbox{\isa{proppat}}}}[]
+\rail@nont{\hyperlink{syntax.prop-pat}{\mbox{\isa{prop{\isaliteral{5F}{\isacharunderscore}}pat}}}}[]
 \rail@endbar
 \rail@nextplus{8}
 \rail@cterm{\isa{\isakeyword{and}}}[]

--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Thu May 05 23:23:02 2011 +0200
@@ -283,7 +283,7 @@
 \rail@endbar
 \rail@bar
 \rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
+\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
 \rail@endbar
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@end