1.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Thu May 08 22:17:37 2008 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Thu May 08 22:20:33 2008 +0200
     1.3 @@ -278,7 +278,7 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \begin{mldecls}
     1.7 -  \indexml{NAMED-CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
     1.8 +  \indexml{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
     1.9    \indexml{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
    1.10    \indexml{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
    1.11    \end{mldecls}
    1.12 @@ -487,7 +487,7 @@
    1.13  \begin{isamarkuptext}%
    1.14  \begin{mldecls}
    1.15    \indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
    1.16 -  \indexml{fold-map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
    1.17 +  \indexml{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
    1.18    \end{mldecls}%
    1.19  \end{isamarkuptext}%
    1.20  \isamarkuptrue%
    1.21 @@ -622,12 +622,12 @@
    1.22  %
    1.23  \begin{isamarkuptext}%
    1.24  \begin{mldecls}
    1.25 -  \indexml{is-some}\verb|is_some: 'a option -> bool| \\
    1.26 -  \indexml{is-none}\verb|is_none: 'a option -> bool| \\
    1.27 +  \indexml{is\_some}\verb|is_some: 'a option -> bool| \\
    1.28 +  \indexml{is\_none}\verb|is_none: 'a option -> bool| \\
    1.29    \indexml{the}\verb|the: 'a option -> 'a| \\
    1.30    \indexml{these}\verb|these: 'a list option -> 'a list| \\
    1.31 -  \indexml{the-list}\verb|the_list: 'a option -> 'a list| \\
    1.32 -  \indexml{the-default}\verb|the_default: 'a -> 'a option -> 'a| \\
    1.33 +  \indexml{the\_list}\verb|the_list: 'a option -> 'a list| \\
    1.34 +  \indexml{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
    1.35    \indexml{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
    1.36    \indexml{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
    1.37    \end{mldecls}%
    1.38 @@ -699,9 +699,9 @@
    1.39    \indexml{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
    1.40    \indexml{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
    1.41    \indexml{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
    1.42 -  \indexml{AList.map-entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
    1.43 +  \indexml{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
    1.44  \verb|    -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list| \\
    1.45 -  \indexml{AList.map-default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
    1.46 +  \indexml{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
    1.47  \verb|    -> ('a * 'b) list -> ('a * 'b) list| \\
    1.48    \indexml{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline%
    1.49  \verb|    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| \\
    1.50 @@ -746,9 +746,9 @@
    1.51    \indexml{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
    1.52    \indexml{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
    1.53  \verb|    -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
    1.54 -  \indexml{Symtab.map-entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
    1.55 +  \indexml{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
    1.56  \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
    1.57 -  \indexml{Symtab.map-default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
    1.58 +  \indexml{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
    1.59  \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
    1.60    \indexml{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
    1.61  \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%

     2.1 --- a/doc-src/IsarImplementation/Thy/document/integration.tex	Thu May 08 22:17:37 2008 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Thu May 08 22:20:33 2008 +0200
     2.3 @@ -84,9 +84,9 @@
     2.4  \begin{mldecls}
     2.5    \indexmltype{Toplevel.state}\verb|type Toplevel.state| \\
     2.6    \indexml{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
     2.7 -  \indexml{Toplevel.is-toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
     2.8 -  \indexml{Toplevel.theory-of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
     2.9 -  \indexml{Toplevel.proof-of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
    2.10 +  \indexml{Toplevel.is\_toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
    2.11 +  \indexml{Toplevel.theory\_of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
    2.12 +  \indexml{Toplevel.proof\_of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
    2.13    \indexml{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
    2.14    \indexml{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
    2.15    \indexml{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
    2.16 @@ -173,18 +173,18 @@
    2.17  \begin{isamarkuptext}%
    2.18  \begin{mldecls}
    2.19    \indexml{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
    2.20 -  \indexml{Toplevel.no-timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
    2.21 +  \indexml{Toplevel.no\_timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
    2.22    \indexml{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
    2.23  \verb|  Toplevel.transition -> Toplevel.transition| \\
    2.24    \indexml{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
    2.25  \verb|  Toplevel.transition -> Toplevel.transition| \\
    2.26 -  \indexml{Toplevel.theory-to-proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
    2.27 +  \indexml{Toplevel.theory\_to\_proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
    2.28  \verb|  Toplevel.transition -> Toplevel.transition| \\
    2.29    \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
    2.30  \verb|  Toplevel.transition -> Toplevel.transition| \\
    2.31    \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
    2.32  \verb|  Toplevel.transition -> Toplevel.transition| \\
    2.33 -  \indexml{Toplevel.end-proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
    2.34 +  \indexml{Toplevel.end\_proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
    2.35  \verb|  Toplevel.transition -> Toplevel.transition| \\
    2.36    \end{mldecls}
    2.37  
    2.38 @@ -301,7 +301,7 @@
    2.39  %
    2.40  \begin{isamarkuptext}%
    2.41  \begin{mldecls}
    2.42 -  \indexml{the-context}\verb|the_context: unit -> theory| \\
    2.43 +  \indexml{the\_context}\verb|the_context: unit -> theory| \\
    2.44    \indexml{Context.$>$$>$ }\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
    2.45    \end{mldecls}
    2.46  
    2.47 @@ -436,15 +436,15 @@
    2.48  \begin{isamarkuptext}%
    2.49  \begin{mldecls}
    2.50    \indexml{theory}\verb|theory: string -> theory| \\
    2.51 -  \indexml{use-thy}\verb|use_thy: string -> unit| \\
    2.52 -  \indexml{use-thys}\verb|use_thys: string list -> unit| \\
    2.53 -  \indexml{touch-thy}\verb|touch_thy: string -> unit| \\
    2.54 -  \indexml{remove-thy}\verb|remove_thy: string -> unit| \\[1ex]
    2.55 -  \indexml{ThyInfo.begin-theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
    2.56 -  \indexml{ThyInfo.end-theory}\verb|ThyInfo.end_theory: theory -> theory| \\
    2.57 -  \indexml{ThyInfo.register-theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
    2.58 +  \indexml{use\_thy}\verb|use_thy: string -> unit| \\
    2.59 +  \indexml{use\_thys}\verb|use_thys: string list -> unit| \\
    2.60 +  \indexml{touch\_thy}\verb|touch_thy: string -> unit| \\
    2.61 +  \indexml{remove\_thy}\verb|remove_thy: string -> unit| \\[1ex]
    2.62 +  \indexml{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
    2.63 +  \indexml{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> theory| \\
    2.64 +  \indexml{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
    2.65    \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
    2.66 -  \indexml{ThyInfo.add-hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
    2.67 +  \indexml{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
    2.68    \end{mldecls}
    2.69  
    2.70    \begin{description}

     3.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Thu May 08 22:17:37 2008 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Thu May 08 22:20:33 2008 +0200
     3.3 @@ -132,18 +132,18 @@
     3.4    \indexmltype{sort}\verb|type sort| \\
     3.5    \indexmltype{arity}\verb|type arity| \\
     3.6    \indexmltype{typ}\verb|type typ| \\
     3.7 -  \indexml{map-atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
     3.8 -  \indexml{fold-atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
     3.9 +  \indexml{map\_atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
    3.10 +  \indexml{fold\_atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
    3.11    \end{mldecls}
    3.12    \begin{mldecls}
    3.13    \indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
    3.14 -  \indexml{Sign.of-sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
    3.15 -  \indexml{Sign.add-types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
    3.16 -  \indexml{Sign.add-tyabbrs-i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
    3.17 +  \indexml{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
    3.18 +  \indexml{Sign.add\_types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
    3.19 +  \indexml{Sign.add\_tyabbrs\_i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
    3.20  \verb|  (string * string list * typ * mixfix) list -> theory -> theory| \\
    3.21 -  \indexml{Sign.primitive-class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
    3.22 -  \indexml{Sign.primitive-classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
    3.23 -  \indexml{Sign.primitive-arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
    3.24 +  \indexml{Sign.primitive\_class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
    3.25 +  \indexml{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
    3.26 +  \indexml{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
    3.27    \end{mldecls}
    3.28  
    3.29    \begin{description}
    3.30 @@ -319,21 +319,21 @@
    3.31  \begin{mldecls}
    3.32    \indexmltype{term}\verb|type term| \\
    3.33    \indexml{op aconv}\verb|op aconv: term * term -> bool| \\
    3.34 -  \indexml{map-types}\verb|map_types: (typ -> typ) -> term -> term| \\
    3.35 -  \indexml{fold-types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
    3.36 -  \indexml{map-aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
    3.37 -  \indexml{fold-aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
    3.38 +  \indexml{map\_types}\verb|map_types: (typ -> typ) -> term -> term| \\
    3.39 +  \indexml{fold\_types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
    3.40 +  \indexml{map\_aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
    3.41 +  \indexml{fold\_aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
    3.42    \end{mldecls}
    3.43    \begin{mldecls}
    3.44 -  \indexml{fastype-of}\verb|fastype_of: term -> typ| \\
    3.45 +  \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
    3.46    \indexml{lambda}\verb|lambda: term -> term -> term| \\
    3.47    \indexml{betapply}\verb|betapply: term * term -> term| \\
    3.48 -  \indexml{Sign.declare-const}\verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix ->|\isasep\isanewline%
    3.49 +  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix ->|\isasep\isanewline%
    3.50  \verb|  theory -> term * theory| \\
    3.51 -  \indexml{Sign.add-abbrev}\verb|Sign.add_abbrev: string -> Markup.property list -> bstring * term ->|\isasep\isanewline%
    3.52 +  \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Markup.property list -> bstring * term ->|\isasep\isanewline%
    3.53  \verb|  theory -> (term * term) * theory| \\
    3.54 -  \indexml{Sign.const-typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
    3.55 -  \indexml{Sign.const-instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
    3.56 +  \indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
    3.57 +  \indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
    3.58    \end{mldecls}
    3.59  
    3.60    \begin{description}
    3.61 @@ -579,27 +579,27 @@
    3.62  \begin{mldecls}
    3.63    \indexmltype{ctyp}\verb|type ctyp| \\
    3.64    \indexmltype{cterm}\verb|type cterm| \\
    3.65 -  \indexml{Thm.ctyp-of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
    3.66 -  \indexml{Thm.cterm-of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
    3.67 +  \indexml{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
    3.68 +  \indexml{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
    3.69    \end{mldecls}
    3.70    \begin{mldecls}
    3.71    \indexmltype{thm}\verb|type thm| \\
    3.72    \indexml{proofs}\verb|proofs: int ref| \\
    3.73    \indexml{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
    3.74 -  \indexml{Thm.forall-intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
    3.75 -  \indexml{Thm.forall-elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
    3.76 -  \indexml{Thm.implies-intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
    3.77 -  \indexml{Thm.implies-elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
    3.78 +  \indexml{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
    3.79 +  \indexml{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
    3.80 +  \indexml{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
    3.81 +  \indexml{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
    3.82    \indexml{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
    3.83    \indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
    3.84 -  \indexml{Thm.get-axiom-i}\verb|Thm.get_axiom_i: theory -> string -> thm| \\
    3.85 -  \indexml{Thm.invoke-oracle-i}\verb|Thm.invoke_oracle_i: theory -> string -> theory * Object.T -> thm| \\
    3.86 +  \indexml{Thm.get\_axiom\_i}\verb|Thm.get_axiom_i: theory -> string -> thm| \\
    3.87 +  \indexml{Thm.invoke\_oracle\_i}\verb|Thm.invoke_oracle_i: theory -> string -> theory * Object.T -> thm| \\
    3.88    \end{mldecls}
    3.89    \begin{mldecls}
    3.90 -  \indexml{Theory.add-axioms-i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\
    3.91 -  \indexml{Theory.add-deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
    3.92 -  \indexml{Theory.add-oracle}\verb|Theory.add_oracle: string * (theory * Object.T -> term) -> theory -> theory| \\
    3.93 -  \indexml{Theory.add-defs-i}\verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory| \\
    3.94 +  \indexml{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\
    3.95 +  \indexml{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
    3.96 +  \indexml{Theory.add\_oracle}\verb|Theory.add_oracle: string * (theory * Object.T -> term) -> theory -> theory| \\
    3.97 +  \indexml{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory| \\
    3.98    \end{mldecls}
    3.99  
   3.100    \begin{description}
   3.101 @@ -739,10 +739,10 @@
   3.102  \begin{mldecls}
   3.103    \indexml{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\
   3.104    \indexml{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\
   3.105 -  \indexml{Drule.mk-term}\verb|Drule.mk_term: cterm -> thm| \\
   3.106 -  \indexml{Drule.dest-term}\verb|Drule.dest_term: thm -> cterm| \\
   3.107 -  \indexml{Logic.mk-type}\verb|Logic.mk_type: typ -> term| \\
   3.108 -  \indexml{Logic.dest-type}\verb|Logic.dest_type: term -> typ| \\
   3.109 +  \indexml{Drule.mk\_term}\verb|Drule.mk_term: cterm -> thm| \\
   3.110 +  \indexml{Drule.dest\_term}\verb|Drule.dest_term: thm -> cterm| \\
   3.111 +  \indexml{Logic.mk\_type}\verb|Logic.mk_type: typ -> term| \\
   3.112 +  \indexml{Logic.dest\_type}\verb|Logic.dest_type: term -> typ| \\
   3.113    \end{mldecls}
   3.114  
   3.115    \begin{description}

     4.1 --- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Thu May 08 22:17:37 2008 +0200
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Thu May 08 22:20:33 2008 +0200
     4.3 @@ -180,9 +180,9 @@
     4.4    \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\
     4.5    \end{mldecls}
     4.6    \begin{mldecls}
     4.7 -  \indexmltype{theory-ref}\verb|type theory_ref| \\
     4.8 +  \indexmltype{theory\_ref}\verb|type theory_ref| \\
     4.9    \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
    4.10 -  \indexml{Theory.check-thy}\verb|Theory.check_thy: theory -> theory_ref| \\
    4.11 +  \indexml{Theory.check\_thy}\verb|Theory.check_thy: theory -> theory_ref| \\
    4.12    \end{mldecls}
    4.13  
    4.14    \begin{description}
    4.15 @@ -276,7 +276,7 @@
    4.16  \begin{mldecls}
    4.17    \indexmltype{Proof.context}\verb|type Proof.context| \\
    4.18    \indexml{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
    4.19 -  \indexml{ProofContext.theory-of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
    4.20 +  \indexml{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
    4.21    \indexml{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
    4.22    \end{mldecls}
    4.23  
    4.24 @@ -334,8 +334,8 @@
    4.25  \begin{isamarkuptext}%
    4.26  \begin{mldecls}
    4.27    \indexmltype{Context.generic}\verb|type Context.generic| \\
    4.28 -  \indexml{Context.theory-of}\verb|Context.theory_of: Context.generic -> theory| \\
    4.29 -  \indexml{Context.proof-of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
    4.30 +  \indexml{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\
    4.31 +  \indexml{Context.proof\_of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
    4.32    \end{mldecls}
    4.33  
    4.34    \begin{description}
    4.35 @@ -553,10 +553,10 @@
    4.36  \begin{mldecls}
    4.37    \indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
    4.38    \indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
    4.39 -  \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
    4.40 -  \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
    4.41 -  \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
    4.42 -  \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
    4.43 +  \indexml{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
    4.44 +  \indexml{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
    4.45 +  \indexml{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
    4.46 +  \indexml{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
    4.47    \end{mldecls}
    4.48    \begin{mldecls}
    4.49    \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
    4.50 @@ -814,8 +814,8 @@
    4.51    \end{mldecls}
    4.52    \begin{mldecls}
    4.53    \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
    4.54 -  \indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
    4.55 -  \indexml{NameSpace.add-path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
    4.56 +  \indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
    4.57 +  \indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
    4.58    \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\
    4.59    \end{mldecls}
    4.60    \begin{mldecls}

     5.1 --- a/doc-src/IsarImplementation/Thy/document/proof.tex	Thu May 08 22:17:37 2008 +0200
     5.2 +++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Thu May 08 22:20:33 2008 +0200
     5.3 @@ -104,15 +104,15 @@
     5.4  %
     5.5  \begin{isamarkuptext}%
     5.6  \begin{mldecls}
     5.7 -  \indexml{Variable.add-fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
     5.8 +  \indexml{Variable.add\_fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
     5.9  \verb|  string list -> Proof.context -> string list * Proof.context| \\
    5.10 -  \indexml{Variable.variant-fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
    5.11 +  \indexml{Variable.variant\_fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
    5.12  \verb|  string list -> Proof.context -> string list * Proof.context| \\
    5.13 -  \indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
    5.14 -  \indexml{Variable.declare-constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
    5.15 +  \indexml{Variable.declare\_term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
    5.16 +  \indexml{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
    5.17    \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
    5.18    \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
    5.19 -  \indexml{Variable.import-thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
    5.20 +  \indexml{Variable.import\_thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
    5.21  \verb|  ((ctyp list * cterm list) * thm list) * Proof.context| \\
    5.22    \indexml{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
    5.23    \end{mldecls}
    5.24 @@ -235,9 +235,9 @@
    5.25  \begin{mldecls}
    5.26    \indexmltype{Assumption.export}\verb|type Assumption.export| \\
    5.27    \indexml{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
    5.28 -  \indexml{Assumption.add-assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
    5.29 +  \indexml{Assumption.add\_assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
    5.30  \verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
    5.31 -  \indexml{Assumption.add-assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
    5.32 +  \indexml{Assumption.add\_assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
    5.33  \verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
    5.34    \indexml{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
    5.35    \end{mldecls}
    5.36 @@ -333,7 +333,7 @@
    5.37    \begin{mldecls}
    5.38    \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
    5.39  \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
    5.40 -  \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
    5.41 +  \indexml{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
    5.42  \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
    5.43    \end{mldecls}
    5.44    \begin{mldecls}

     6.1 --- a/doc-src/IsarImplementation/implementation.tex	Thu May 08 22:17:37 2008 +0200
     6.2 +++ b/doc-src/IsarImplementation/implementation.tex	Thu May 08 22:20:33 2008 +0200
     6.3 @@ -5,6 +5,7 @@
     6.4  \usepackage{latexsym,graphicx}
     6.5  \usepackage[refpage]{nomencl}
     6.6  \usepackage{../iman,../extra,../isar,../proof}
     6.7 +\usepackage[nohyphen,strings]{underscore}
     6.8  \usepackage{Thy/document/isabelle,Thy/document/isabellesym}
     6.9  \usepackage{style}
    6.10  \usepackage{../pdfsetup}

     7.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Thu May 08 22:17:37 2008 +0200
     7.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Thu May 08 22:20:33 2008 +0200
     7.3 @@ -38,9 +38,9 @@
     7.4      \indexdef{}{command}{definition}\mbox{\isa{\isacommand{definition}}} & : & \isarkeep{local{\dsh}theory} \\
     7.5      \indexdef{}{attribute}{defn}\mbox{\isa{defn}} & : & \isaratt \\
     7.6      \indexdef{}{command}{abbreviation}\mbox{\isa{\isacommand{abbreviation}}} & : & \isarkeep{local{\dsh}theory} \\
     7.7 -    \indexdef{}{command}{print-abbrevs}\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
     7.8 +    \indexdef{}{command}{print\_abbrevs}\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
     7.9      \indexdef{}{command}{notation}\mbox{\isa{\isacommand{notation}}} & : & \isarkeep{local{\dsh}theory} \\
    7.10 -    \indexdef{}{command}{no-notation}\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}} & : & \isarkeep{local{\dsh}theory} \\
    7.11 +    \indexdef{}{command}{no\_notation}\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}} & : & \isarkeep{local{\dsh}theory} \\
    7.12    \end{matharray}
    7.13  
    7.14    These specification mechanisms provide a slightly more abstract view
    7.15 @@ -256,10 +256,10 @@
    7.16  \begin{isamarkuptext}%
    7.17  \begin{matharray}{rcl}
    7.18      \indexdef{}{command}{locale}\mbox{\isa{\isacommand{locale}}} & : & \isartrans{theory}{local{\dsh}theory} \\
    7.19 -    \indexdef{}{command}{print-locale}\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    7.20 -    \indexdef{}{command}{print-locales}\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    7.21 -    \indexdef{}{method}{intro-locales}\mbox{\isa{intro{\isacharunderscore}locales}} & : & \isarmeth \\
    7.22 -    \indexdef{}{method}{unfold-locales}\mbox{\isa{unfold{\isacharunderscore}locales}} & : & \isarmeth \\
    7.23 +    \indexdef{}{command}{print\_locale}\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    7.24 +    \indexdef{}{command}{print\_locales}\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    7.25 +    \indexdef{}{method}{intro\_locales}\mbox{\isa{intro{\isacharunderscore}locales}} & : & \isarmeth \\
    7.26 +    \indexdef{}{method}{unfold\_locales}\mbox{\isa{unfold{\isacharunderscore}locales}} & : & \isarmeth \\
    7.27    \end{matharray}
    7.28  
    7.29    \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
    7.30 @@ -421,7 +421,7 @@
    7.31    \begin{matharray}{rcl}
    7.32      \indexdef{}{command}{interpretation}\mbox{\isa{\isacommand{interpretation}}} & : & \isartrans{theory}{proof(prove)} \\
    7.33      \indexdef{}{command}{interpret}\mbox{\isa{\isacommand{interpret}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
    7.34 -    \indexdef{}{command}{print-interps}\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : &  \isarkeep{theory~|~proof} \\
    7.35 +    \indexdef{}{command}{print\_interps}\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : &  \isarkeep{theory~|~proof} \\
    7.36    \end{matharray}
    7.37  
    7.38    \indexouternonterm{interp}
    7.39 @@ -560,8 +560,8 @@
    7.40      \indexdef{}{command}{instantiation}\mbox{\isa{\isacommand{instantiation}}} & : & \isartrans{theory}{local{\dsh}theory} \\
    7.41      \indexdef{}{command}{instance}\mbox{\isa{\isacommand{instance}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
    7.42      \indexdef{}{command}{subclass}\mbox{\isa{\isacommand{subclass}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
    7.43 -    \indexdef{}{command}{print-classes}\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    7.44 -    \indexdef{}{method}{intro-classes}\mbox{\isa{intro{\isacharunderscore}classes}} & : & \isarmeth \\
    7.45 +    \indexdef{}{command}{print\_classes}\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    7.46 +    \indexdef{}{method}{intro\_classes}\mbox{\isa{intro{\isacharunderscore}classes}} & : & \isarmeth \\
    7.47    \end{matharray}
    7.48  
    7.49    \begin{rail}
    7.50 @@ -769,7 +769,7 @@
    7.51    ``global'', which may not be changed within a local context.
    7.52  
    7.53    \begin{matharray}{rcll}
    7.54 -    \indexdef{}{command}{print-configs}\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}} & : & \isarkeep{theory~|~proof} \\
    7.55 +    \indexdef{}{command}{print\_configs}\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}} & : & \isarkeep{theory~|~proof} \\
    7.56    \end{matharray}
    7.57  
    7.58    \begin{rail}
    7.59 @@ -881,7 +881,7 @@
    7.60      \indexdef{}{command}{finally}\mbox{\isa{\isacommand{finally}}} & : & \isartrans{proof(state)}{proof(chain)} \\
    7.61      \indexdef{}{command}{moreover}\mbox{\isa{\isacommand{moreover}}} & : & \isartrans{proof(state)}{proof(state)} \\
    7.62      \indexdef{}{command}{ultimately}\mbox{\isa{\isacommand{ultimately}}} & : & \isartrans{proof(state)}{proof(chain)} \\
    7.63 -    \indexdef{}{command}{print-trans-rules}\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    7.64 +    \indexdef{}{command}{print\_trans\_rules}\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    7.65      \mbox{\isa{trans}} & : & \isaratt \\
    7.66      \mbox{\isa{sym}} & : & \isaratt \\
    7.67      \mbox{\isa{symmetric}} & : & \isaratt \\
    7.68 @@ -1045,9 +1045,9 @@
    7.69      \indexdef{}{attribute}{unfolded}\mbox{\isa{unfolded}} & : & \isaratt \\
    7.70      \indexdef{}{attribute}{folded}\mbox{\isa{folded}} & : & \isaratt \\[0.5ex]
    7.71      \indexdef{}{attribute}{rotated}\mbox{\isa{rotated}} & : & \isaratt \\
    7.72 -    \indexdef{Pure}{attribute}{elim-format}\mbox{\isa{elim{\isacharunderscore}format}} & : & \isaratt \\
    7.73 +    \indexdef{Pure}{attribute}{elim\_format}\mbox{\isa{elim{\isacharunderscore}format}} & : & \isaratt \\
    7.74      \indexdef{}{attribute}{standard}\mbox{\isa{standard}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
    7.75 -    \indexdef{}{attribute}{no-vars}\mbox{\isa{no{\isacharunderscore}vars}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
    7.76 +    \indexdef{}{attribute}{no\_vars}\mbox{\isa{no{\isacharunderscore}vars}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
    7.77    \end{matharray}
    7.78  
    7.79    \begin{rail}
    7.80 @@ -1135,15 +1135,15 @@
    7.81    \secref{sec:pure-meth-att}).
    7.82  
    7.83    \begin{matharray}{rcl}
    7.84 -    \indexdef{}{method}{rule-tac}\mbox{\isa{rule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.85 -    \indexdef{}{method}{erule-tac}\mbox{\isa{erule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.86 -    \indexdef{}{method}{drule-tac}\mbox{\isa{drule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.87 -    \indexdef{}{method}{frule-tac}\mbox{\isa{frule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.88 -    \indexdef{}{method}{cut-tac}\mbox{\isa{cut{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.89 -    \indexdef{}{method}{thin-tac}\mbox{\isa{thin{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.90 -    \indexdef{}{method}{subgoal-tac}\mbox{\isa{subgoal{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.91 -    \indexdef{}{method}{rename-tac}\mbox{\isa{rename{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.92 -    \indexdef{}{method}{rotate-tac}\mbox{\isa{rotate{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.93 +    \indexdef{}{method}{rule\_tac}\mbox{\isa{rule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.94 +    \indexdef{}{method}{erule\_tac}\mbox{\isa{erule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.95 +    \indexdef{}{method}{drule\_tac}\mbox{\isa{drule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.96 +    \indexdef{}{method}{frule\_tac}\mbox{\isa{frule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.97 +    \indexdef{}{method}{cut\_tac}\mbox{\isa{cut{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.98 +    \indexdef{}{method}{thin\_tac}\mbox{\isa{thin{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    7.99 +    \indexdef{}{method}{subgoal\_tac}\mbox{\isa{subgoal{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
   7.100 +    \indexdef{}{method}{rename\_tac}\mbox{\isa{rename{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
   7.101 +    \indexdef{}{method}{rotate\_tac}\mbox{\isa{rotate{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
   7.102      \indexdef{}{method}{tactic}\mbox{\isa{tactic}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
   7.103    \end{matharray}
   7.104  
   7.105 @@ -1227,7 +1227,7 @@
   7.106  \begin{isamarkuptext}%
   7.107  \begin{matharray}{rcl}
   7.108      \indexdef{}{method}{simp}\mbox{\isa{simp}} & : & \isarmeth \\
   7.109 -    \indexdef{}{method}{simp-all}\mbox{\isa{simp{\isacharunderscore}all}} & : & \isarmeth \\
   7.110 +    \indexdef{}{method}{simp\_all}\mbox{\isa{simp{\isacharunderscore}all}} & : & \isarmeth \\
   7.111    \end{matharray}
   7.112  
   7.113    \indexouternonterm{simpmod}
   7.114 @@ -1301,7 +1301,7 @@
   7.115  %
   7.116  \begin{isamarkuptext}%
   7.117  \begin{matharray}{rcl}
   7.118 -    \indexdef{}{command}{print-simpset}\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   7.119 +    \indexdef{}{command}{print\_simpset}\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   7.120      \indexdef{}{attribute}{simp}\mbox{\isa{simp}} & : & \isaratt \\
   7.121      \indexdef{}{attribute}{cong}\mbox{\isa{cong}} & : & \isaratt \\
   7.122      \indexdef{}{attribute}{split}\mbox{\isa{split}} & : & \isaratt \\
   7.123 @@ -1334,7 +1334,7 @@
   7.124  %
   7.125  \begin{isamarkuptext}%
   7.126  \begin{matharray}{rcl}
   7.127 -    \indexdef{}{command}{simproc-setup}\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}} & : & \isarkeep{local{\dsh}theory} \\
   7.128 +    \indexdef{}{command}{simproc\_setup}\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}} & : & \isarkeep{local{\dsh}theory} \\
   7.129      simproc & : & \isaratt \\
   7.130    \end{matharray}
   7.131  
   7.132 @@ -1621,7 +1621,7 @@
   7.133  %
   7.134  \begin{isamarkuptext}%
   7.135  \begin{matharray}{rcl}
   7.136 -    \indexdef{}{command}{print-claset}\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   7.137 +    \indexdef{}{command}{print\_claset}\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   7.138      \indexdef{}{attribute}{intro}\mbox{\isa{intro}} & : & \isaratt \\
   7.139      \indexdef{}{attribute}{elim}\mbox{\isa{elim}} & : & \isaratt \\
   7.140      \indexdef{}{attribute}{dest}\mbox{\isa{dest}} & : & \isaratt \\
   7.141 @@ -1700,9 +1700,9 @@
   7.142  \begin{isamarkuptext}%
   7.143  \begin{matharray}{rcl}
   7.144      \indexdef{}{command}{case}\mbox{\isa{\isacommand{case}}} & : & \isartrans{proof(state)}{proof(state)} \\
   7.145 -    \indexdef{}{command}{print-cases}\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
   7.146 -    \indexdef{}{attribute}{case-names}\mbox{\isa{case{\isacharunderscore}names}} & : & \isaratt \\
   7.147 -    \indexdef{}{attribute}{case-conclusion}\mbox{\isa{case{\isacharunderscore}conclusion}} & : & \isaratt \\
   7.148 +    \indexdef{}{command}{print\_cases}\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
   7.149 +    \indexdef{}{attribute}{case\_names}\mbox{\isa{case{\isacharunderscore}names}} & : & \isaratt \\
   7.150 +    \indexdef{}{attribute}{case\_conclusion}\mbox{\isa{case{\isacharunderscore}conclusion}} & : & \isaratt \\
   7.151      \indexdef{}{attribute}{params}\mbox{\isa{params}} & : & \isaratt \\
   7.152      \indexdef{}{attribute}{consumes}\mbox{\isa{consumes}} & : & \isaratt \\
   7.153    \end{matharray}
   7.154 @@ -2000,7 +2000,7 @@
   7.155  %
   7.156  \begin{isamarkuptext}%
   7.157  \begin{matharray}{rcl}
   7.158 -    \indexdef{}{command}{print-induct-rules}\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   7.159 +    \indexdef{}{command}{print\_induct\_rules}\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   7.160      \indexdef{}{attribute}{cases}\mbox{\isa{cases}} & : & \isaratt \\
   7.161      \indexdef{}{attribute}{induct}\mbox{\isa{induct}} & : & \isaratt \\
   7.162      \indexdef{}{attribute}{coinduct}\mbox{\isa{coinduct}} & : & \isaratt \\
   7.163 @@ -2047,7 +2047,7 @@
   7.164      \indexdef{}{command}{judgment}\mbox{\isa{\isacommand{judgment}}} & : & \isartrans{theory}{theory} \\
   7.165      \indexdef{}{method}{atomize}\mbox{\isa{atomize}} & : & \isarmeth \\
   7.166      \indexdef{}{attribute}{atomize}\mbox{\isa{atomize}} & : & \isaratt \\
   7.167 -    \indexdef{}{attribute}{rule-format}\mbox{\isa{rule{\isacharunderscore}format}} & : & \isaratt \\
   7.168 +    \indexdef{}{attribute}{rule\_format}\mbox{\isa{rule{\isacharunderscore}format}} & : & \isaratt \\
   7.169      \indexdef{}{attribute}{rulify}\mbox{\isa{rulify}} & : & \isaratt \\
   7.170    \end{matharray}
   7.171  

     8.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 22:17:37 2008 +0200
     8.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 22:20:33 2008 +0200
     8.3 @@ -364,7 +364,7 @@
     8.4  \begin{isamarkuptext}%
     8.5  \begin{matharray}{rcl}
     8.6      \indexdef{HOL}{command}{datatype}\mbox{\isa{\isacommand{datatype}}} & : & \isartrans{theory}{theory} \\
     8.7 -    \indexdef{HOL}{command}{rep-datatype}\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
     8.8 +    \indexdef{HOL}{command}{rep\_datatype}\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
     8.9    \end{matharray}
    8.10  
    8.11    \begin{rail}
    8.12 @@ -517,9 +517,9 @@
    8.13  %
    8.14  \begin{isamarkuptext}%
    8.15  \begin{matharray}{rcl}
    8.16 -    \indexdef{HOL}{method}{pat-completeness}\mbox{\isa{pat{\isacharunderscore}completeness}} & : & \isarmeth \\
    8.17 +    \indexdef{HOL}{method}{pat\_completeness}\mbox{\isa{pat{\isacharunderscore}completeness}} & : & \isarmeth \\
    8.18      \indexdef{HOL}{method}{relation}\mbox{\isa{relation}} & : & \isarmeth \\
    8.19 -    \indexdef{HOL}{method}{lexicographic-order}\mbox{\isa{lexicographic{\isacharunderscore}order}} & : & \isarmeth \\
    8.20 +    \indexdef{HOL}{method}{lexicographic\_order}\mbox{\isa{lexicographic{\isacharunderscore}order}} & : & \isarmeth \\
    8.21    \end{matharray}
    8.22  
    8.23    \begin{rail}
    8.24 @@ -567,7 +567,7 @@
    8.25  
    8.26    \begin{matharray}{rcl}
    8.27      \indexdef{HOL}{command}{recdef}\mbox{\isa{\isacommand{recdef}}} & : & \isartrans{theory}{theory} \\
    8.28 -    \indexdef{HOL}{command}{recdef-tc}\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\
    8.29 +    \indexdef{HOL}{command}{recdef\_tc}\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\
    8.30    \end{matharray}
    8.31  
    8.32    \begin{rail}
    8.33 @@ -609,9 +609,9 @@
    8.34    globally, using the following attributes.
    8.35  
    8.36    \begin{matharray}{rcl}
    8.37 -    \indexdef{HOL}{attribute}{recdef-simp}\mbox{\isa{recdef{\isacharunderscore}simp}} & : & \isaratt \\
    8.38 -    \indexdef{HOL}{attribute}{recdef-cong}\mbox{\isa{recdef{\isacharunderscore}cong}} & : & \isaratt \\
    8.39 -    \indexdef{HOL}{attribute}{recdef-wf}\mbox{\isa{recdef{\isacharunderscore}wf}} & : & \isaratt \\
    8.40 +    \indexdef{HOL}{attribute}{recdef\_simp}\mbox{\isa{recdef{\isacharunderscore}simp}} & : & \isaratt \\
    8.41 +    \indexdef{HOL}{attribute}{recdef\_cong}\mbox{\isa{recdef{\isacharunderscore}cong}} & : & \isaratt \\
    8.42 +    \indexdef{HOL}{attribute}{recdef\_wf}\mbox{\isa{recdef{\isacharunderscore}wf}} & : & \isaratt \\
    8.43    \end{matharray}
    8.44  
    8.45    \begin{rail}
    8.46 @@ -628,7 +628,7 @@
    8.47  \begin{isamarkuptext}%
    8.48  \begin{matharray}{rcl}
    8.49      \indexdef{HOL}{command}{specification}\mbox{\isa{\isacommand{specification}}} & : & \isartrans{theory}{proof(prove)} \\
    8.50 -    \indexdef{HOL}{command}{ax-specification}\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} & : & \isartrans{theory}{proof(prove)} \\
    8.51 +    \indexdef{HOL}{command}{ax\_specification}\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} & : & \isartrans{theory}{proof(prove)} \\
    8.52    \end{matharray}
    8.53  
    8.54    \begin{rail}
    8.55 @@ -698,9 +698,9 @@
    8.56  
    8.57    \begin{matharray}{rcl}
    8.58      \indexdef{HOL}{command}{inductive}\mbox{\isa{\isacommand{inductive}}} & : & \isarkeep{local{\dsh}theory} \\
    8.59 -    \indexdef{HOL}{command}{inductive-set}\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
    8.60 +    \indexdef{HOL}{command}{inductive\_set}\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
    8.61      \indexdef{HOL}{command}{coinductive}\mbox{\isa{\isacommand{coinductive}}} & : & \isarkeep{local{\dsh}theory} \\
    8.62 -    \indexdef{HOL}{command}{coinductive-set}\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
    8.63 +    \indexdef{HOL}{command}{coinductive\_set}\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
    8.64      \indexdef{HOL}{attribute}{mono}\mbox{\isa{mono}} & : & \isaratt \\
    8.65    \end{matharray}
    8.66  
    8.67 @@ -817,7 +817,7 @@
    8.68  \begin{isamarkuptext}%
    8.69  \begin{matharray}{rcl}
    8.70      \indexdef{HOL}{method}{arith}\mbox{\isa{arith}} & : & \isarmeth \\
    8.71 -    \indexdef{HOL}{method}{arith-split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
    8.72 +    \indexdef{HOL}{method}{arith\_split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
    8.73    \end{matharray}
    8.74  
    8.75    The \mbox{\isa{arith}} method decides linear arithmetic problems
    8.76 @@ -841,10 +841,10 @@
    8.77    ported to Isar.  These should be never used in proper proof texts!
    8.78  
    8.79    \begin{matharray}{rcl}
    8.80 -    \indexdef{HOL}{method}{case-tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    8.81 -    \indexdef{HOL}{method}{induct-tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    8.82 -    \indexdef{HOL}{method}{ind-cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    8.83 -    \indexdef{HOL}{command}{inductive-cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
    8.84 +    \indexdef{HOL}{method}{case\_tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    8.85 +    \indexdef{HOL}{method}{induct\_tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    8.86 +    \indexdef{HOL}{method}{ind\_cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    8.87 +    \indexdef{HOL}{command}{inductive\_cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
    8.88    \end{matharray}
    8.89  
    8.90    \begin{rail}
    8.91 @@ -900,10 +900,10 @@
    8.92  
    8.93    \begin{matharray}{rcl}
    8.94      \indexdef{HOL}{command}{value}\mbox{\isa{\isacommand{value}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
    8.95 -    \indexdef{HOL}{command}{code-module}\mbox{\isa{\isacommand{code{\isacharunderscore}module}}} & : & \isartrans{theory}{theory} \\
    8.96 -    \indexdef{HOL}{command}{code-library}\mbox{\isa{\isacommand{code{\isacharunderscore}library}}} & : & \isartrans{theory}{theory} \\
    8.97 -    \indexdef{HOL}{command}{consts-code}\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\
    8.98 -    \indexdef{HOL}{command}{types-code}\mbox{\isa{\isacommand{types{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\  
    8.99 +    \indexdef{HOL}{command}{code\_module}\mbox{\isa{\isacommand{code{\isacharunderscore}module}}} & : & \isartrans{theory}{theory} \\
   8.100 +    \indexdef{HOL}{command}{code\_library}\mbox{\isa{\isacommand{code{\isacharunderscore}library}}} & : & \isartrans{theory}{theory} \\
   8.101 +    \indexdef{HOL}{command}{consts\_code}\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\
   8.102 +    \indexdef{HOL}{command}{types\_code}\mbox{\isa{\isacommand{types{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\  
   8.103      \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\
   8.104    \end{matharray}
   8.105  
   8.106 @@ -961,20 +961,20 @@
   8.107    introduction on how to use it.
   8.108  
   8.109    \begin{matharray}{rcl}
   8.110 -    \indexdef{HOL}{command}{export-code}\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   8.111 -    \indexdef{HOL}{command}{code-thms}\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   8.112 -    \indexdef{HOL}{command}{code-deps}\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   8.113 -    \indexdef{HOL}{command}{code-datatype}\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
   8.114 -    \indexdef{HOL}{command}{code-const}\mbox{\isa{\isacommand{code{\isacharunderscore}const}}} & : & \isartrans{theory}{theory} \\
   8.115 -    \indexdef{HOL}{command}{code-type}\mbox{\isa{\isacommand{code{\isacharunderscore}type}}} & : & \isartrans{theory}{theory} \\
   8.116 -    \indexdef{HOL}{command}{code-class}\mbox{\isa{\isacommand{code{\isacharunderscore}class}}} & : & \isartrans{theory}{theory} \\
   8.117 -    \indexdef{HOL}{command}{code-instance}\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}} & : & \isartrans{theory}{theory} \\
   8.118 -    \indexdef{HOL}{command}{code-monad}\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}} & : & \isartrans{theory}{theory} \\
   8.119 -    \indexdef{HOL}{command}{code-reserved}\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}} & : & \isartrans{theory}{theory} \\
   8.120 -    \indexdef{HOL}{command}{code-include}\mbox{\isa{\isacommand{code{\isacharunderscore}include}}} & : & \isartrans{theory}{theory} \\
   8.121 -    \indexdef{HOL}{command}{code-modulename}\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}} & : & \isartrans{theory}{theory} \\
   8.122 -    \indexdef{HOL}{command}{code-exception}\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}} & : & \isartrans{theory}{theory} \\
   8.123 -    \indexdef{HOL}{command}{print-codesetup}\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   8.124 +    \indexdef{HOL}{command}{export\_code}\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   8.125 +    \indexdef{HOL}{command}{code\_thms}\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   8.126 +    \indexdef{HOL}{command}{code\_deps}\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   8.127 +    \indexdef{HOL}{command}{code\_datatype}\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
   8.128 +    \indexdef{HOL}{command}{code\_const}\mbox{\isa{\isacommand{code{\isacharunderscore}const}}} & : & \isartrans{theory}{theory} \\
   8.129 +    \indexdef{HOL}{command}{code\_type}\mbox{\isa{\isacommand{code{\isacharunderscore}type}}} & : & \isartrans{theory}{theory} \\
   8.130 +    \indexdef{HOL}{command}{code\_class}\mbox{\isa{\isacommand{code{\isacharunderscore}class}}} & : & \isartrans{theory}{theory} \\
   8.131 +    \indexdef{HOL}{command}{code\_instance}\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}} & : & \isartrans{theory}{theory} \\
   8.132 +    \indexdef{HOL}{command}{code\_monad}\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}} & : & \isartrans{theory}{theory} \\
   8.133 +    \indexdef{HOL}{command}{code\_reserved}\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}} & : & \isartrans{theory}{theory} \\
   8.134 +    \indexdef{HOL}{command}{code\_include}\mbox{\isa{\isacommand{code{\isacharunderscore}include}}} & : & \isartrans{theory}{theory} \\
   8.135 +    \indexdef{HOL}{command}{code\_modulename}\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}} & : & \isartrans{theory}{theory} \\
   8.136 +    \indexdef{HOL}{command}{code\_exception}\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}} & : & \isartrans{theory}{theory} \\
   8.137 +    \indexdef{HOL}{command}{print\_codesetup}\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
   8.138      \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\
   8.139    \end{matharray}
   8.140  

     9.1 --- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Thu May 08 22:17:37 2008 +0200
     9.2 +++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex	Thu May 08 22:20:33 2008 +0200
     9.3 @@ -36,7 +36,7 @@
     9.4    Simplifier setup.
     9.5  
     9.6    \begin{matharray}{rcl}
     9.7 -    \indexdef{ZF}{command}{print-tcset}\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
     9.8 +    \indexdef{ZF}{command}{print\_tcset}\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
     9.9      \indexdef{ZF}{method}{typecheck}\mbox{\isa{typecheck}} & : & \isarmeth \\
    9.10      \indexdef{ZF}{attribute}{TC}\mbox{\isa{TC}} & : & \isaratt \\
    9.11    \end{matharray}
    9.12 @@ -148,10 +148,10 @@
    9.13    ported to Isar.  These should not be used in proper proof texts.
    9.14  
    9.15    \begin{matharray}{rcl}
    9.16 -    \indexdef{ZF}{method}{case-tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    9.17 -    \indexdef{ZF}{method}{induct-tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    9.18 -    \indexdef{ZF}{method}{ind-cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    9.19 -    \indexdef{ZF}{command}{inductive-cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
    9.20 +    \indexdef{ZF}{method}{case\_tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    9.21 +    \indexdef{ZF}{method}{induct\_tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    9.22 +    \indexdef{ZF}{method}{ind\_cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
    9.23 +    \indexdef{ZF}{command}{inductive\_cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
    9.24    \end{matharray}
    9.25  
    9.26    \begin{rail}

    10.1 --- a/doc-src/IsarRef/Thy/document/pure.tex	Thu May 08 22:17:37 2008 +0200
    10.2 +++ b/doc-src/IsarRef/Thy/document/pure.tex	Thu May 08 22:20:33 2008 +0200
    10.3 @@ -128,7 +128,7 @@
    10.4      \indexdef{}{command}{subsection}\mbox{\isa{\isacommand{subsection}}} & : & \isarkeep{local{\dsh}theory} \\
    10.5      \indexdef{}{command}{subsubsection}\mbox{\isa{\isacommand{subsubsection}}} & : & \isarkeep{local{\dsh}theory} \\
    10.6      \indexdef{}{command}{text}\mbox{\isa{\isacommand{text}}} & : & \isarkeep{local{\dsh}theory} \\
    10.7 -    \indexdef{}{command}{text-raw}\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}} & : & \isarkeep{local{\dsh}theory} \\
    10.8 +    \indexdef{}{command}{text\_raw}\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}} & : & \isarkeep{local{\dsh}theory} \\
    10.9    \end{matharray}
   10.10  
   10.11    Apart from formal comments (see \secref{sec:comments}), markup
   10.12 @@ -184,7 +184,7 @@
   10.13      \indexdef{}{command}{classes}\mbox{\isa{\isacommand{classes}}} & : & \isartrans{theory}{theory} \\
   10.14      \indexdef{}{command}{classrel}\mbox{\isa{\isacommand{classrel}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
   10.15      \indexdef{}{command}{defaultsort}\mbox{\isa{\isacommand{defaultsort}}} & : & \isartrans{theory}{theory} \\
   10.16 -    \indexdef{}{command}{class-deps}\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}} & : & \isarkeep{theory~|~proof} \\
   10.17 +    \indexdef{}{command}{class\_deps}\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}} & : & \isarkeep{theory~|~proof} \\
   10.18    \end{matharray}
   10.19  
   10.20    \begin{rail}
   10.21 @@ -380,9 +380,9 @@
   10.22  \begin{isamarkuptext}%
   10.23  \begin{matharray}{rcl}
   10.24      \indexdef{}{command}{syntax}\mbox{\isa{\isacommand{syntax}}} & : & \isartrans{theory}{theory} \\
   10.25 -    \indexdef{}{command}{no-syntax}\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}} & : & \isartrans{theory}{theory} \\
   10.26 +    \indexdef{}{command}{no\_syntax}\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}} & : & \isartrans{theory}{theory} \\
   10.27      \indexdef{}{command}{translations}\mbox{\isa{\isacommand{translations}}} & : & \isartrans{theory}{theory} \\
   10.28 -    \indexdef{}{command}{no-translations}\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}} & : & \isartrans{theory}{theory} \\
   10.29 +    \indexdef{}{command}{no\_translations}\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}} & : & \isartrans{theory}{theory} \\
   10.30    \end{matharray}
   10.31  
   10.32    \begin{rail}
   10.33 @@ -521,10 +521,10 @@
   10.34  \begin{matharray}{rcl}
   10.35      \indexdef{}{command}{use}\mbox{\isa{\isacommand{use}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
   10.36      \indexdef{}{command}{ML}\mbox{\isa{\isacommand{ML}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
   10.37 -    \indexdef{}{command}{ML-val}\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}} & : & \isartrans{\cdot}{\cdot} \\
   10.38 -    \indexdef{}{command}{ML-command}\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}} & : & \isartrans{\cdot}{\cdot} \\
   10.39 +    \indexdef{}{command}{ML\_val}\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}} & : & \isartrans{\cdot}{\cdot} \\
   10.40 +    \indexdef{}{command}{ML\_command}\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}} & : & \isartrans{\cdot}{\cdot} \\
   10.41      \indexdef{}{command}{setup}\mbox{\isa{\isacommand{setup}}} & : & \isartrans{theory}{theory} \\
   10.42 -    \indexdef{}{command}{method-setup}\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}} & : & \isartrans{theory}{theory} \\
   10.43 +    \indexdef{}{command}{method\_setup}\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}} & : & \isartrans{theory}{theory} \\
   10.44    \end{matharray}
   10.45  
   10.46    \begin{rail}
   10.47 @@ -591,12 +591,12 @@
   10.48  %
   10.49  \begin{isamarkuptext}%
   10.50  \begin{matharray}{rcl}
   10.51 -    \indexdef{}{command}{parse-ast-translation}\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
   10.52 -    \indexdef{}{command}{parse-translation}\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
   10.53 -    \indexdef{}{command}{print-translation}\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
   10.54 -    \indexdef{}{command}{typed-print-translation}\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
   10.55 -    \indexdef{}{command}{print-ast-translation}\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
   10.56 -    \indexdef{}{command}{token-translation}\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
   10.57 +    \indexdef{}{command}{parse\_ast\_translation}\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
   10.58 +    \indexdef{}{command}{parse\_translation}\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
   10.59 +    \indexdef{}{command}{print\_translation}\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
   10.60 +    \indexdef{}{command}{typed\_print\_translation}\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
   10.61 +    \indexdef{}{command}{print\_ast\_translation}\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
   10.62 +    \indexdef{}{command}{token\_translation}\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
   10.63    \end{matharray}
   10.64  
   10.65    \begin{rail}
   10.66 @@ -734,7 +734,7 @@
   10.67      \indexdef{}{command}{subsect}\mbox{\isa{\isacommand{subsect}}} & : & \isartrans{proof}{proof} \\
   10.68      \indexdef{}{command}{subsubsect}\mbox{\isa{\isacommand{subsubsect}}} & : & \isartrans{proof}{proof} \\
   10.69      \indexdef{}{command}{txt}\mbox{\isa{\isacommand{txt}}} & : & \isartrans{proof}{proof} \\
   10.70 -    \indexdef{}{command}{txt-raw}\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}} & : & \isartrans{proof}{proof} \\
   10.71 +    \indexdef{}{command}{txt\_raw}\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}} & : & \isartrans{proof}{proof} \\
   10.72    \end{matharray}
   10.73  
   10.74    These markup commands for proof mode closely correspond to the ones
   10.75 @@ -905,7 +905,7 @@
   10.76    of the premises of the rule involved.  Note that positions may be
   10.77    easily skipped using something like \mbox{\isa{\isacommand{from}}}~\isa{{\isachardoublequote}{\isacharunderscore}\ {\isasymAND}\ a\ {\isasymAND}\ b{\isachardoublequote}}, for example.  This involves the trivial rule
   10.78    \isa{{\isachardoublequote}PROP\ {\isasympsi}\ {\isasymLongrightarrow}\ PROP\ {\isasympsi}{\isachardoublequote}}, which is bound in Isabelle/Pure as
   10.79 -  ``\indexref{}{fact}{-}\mbox{\isa{{\isacharunderscore}}}'' (underscore).
   10.80 +  ``\indexref{}{fact}{\_}\mbox{\isa{{\isacharunderscore}}}'' (underscore).
   10.81  
   10.82    Automated methods (such as \mbox{\isa{simp}} or \mbox{\isa{auto}}) just
   10.83    insert any given facts before their usual operation.  Depending on
   10.84 @@ -1032,7 +1032,7 @@
   10.85    Any goal statement causes some term abbreviations (such as
   10.86    \indexref{}{variable}{?thesis}\mbox{\isa{{\isacharquery}thesis}}) to be bound automatically, see also
   10.87    \secref{sec:term-abbrev}.  Furthermore, the local context of a
   10.88 -  (non-atomic) goal is provided via the \indexref{}{case}{rule-context}\mbox{\isa{rule{\isacharunderscore}context}} case.
   10.89 +  (non-atomic) goal is provided via the \indexref{}{case}{rule\_context}\mbox{\isa{rule{\isacharunderscore}context}} case.
   10.90  
   10.91    The optional case names of \indexref{}{element}{obtains}\mbox{\isa{\isakeyword{obtains}}} have a twofold
   10.92    meaning: (1) during the of this claim they refer to the the local
   10.93 @@ -1430,7 +1430,7 @@
   10.94  
   10.95    \begin{matharray}{rcl}
   10.96      \indexdef{}{command}{apply}\mbox{\isa{\isacommand{apply}}}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
   10.97 -    \indexdef{}{command}{apply-end}\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}^* & : & \isartrans{proof(state)}{proof(state)} \\
   10.98 +    \indexdef{}{command}{apply\_end}\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}^* & : & \isartrans{proof(state)}{proof(state)} \\
   10.99      \indexdef{}{command}{done}\mbox{\isa{\isacommand{done}}}^* & : & \isartrans{proof(prove)}{proof(state)} \\
  10.100      \indexdef{}{command}{defer}\mbox{\isa{\isacommand{defer}}}^* & : & \isartrans{proof}{proof} \\
  10.101      \indexdef{}{command}{prefer}\mbox{\isa{\isacommand{prefer}}}^* & : & \isartrans{proof}{proof} \\
  10.102 @@ -1621,16 +1621,16 @@
  10.103  %
  10.104  \begin{isamarkuptext}%
  10.105  \begin{matharray}{rcl}
  10.106 -    \indexdef{}{command}{print-commands}\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}^* & : & \isarkeep{\cdot} \\
  10.107 -    \indexdef{}{command}{print-theory}\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}^* & : & \isarkeep{theory~|~proof} \\
  10.108 -    \indexdef{}{command}{print-syntax}\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}^* & : & \isarkeep{theory~|~proof} \\
  10.109 -    \indexdef{}{command}{print-methods}\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}^* & : & \isarkeep{theory~|~proof} \\
  10.110 -    \indexdef{}{command}{print-attributes}\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}^* & : & \isarkeep{theory~|~proof} \\
  10.111 -    \indexdef{}{command}{print-theorems}\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}^* & : & \isarkeep{theory~|~proof} \\
  10.112 -    \indexdef{}{command}{find-theorems}\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}^* & : & \isarkeep{theory~|~proof} \\
  10.113 -    \indexdef{}{command}{thms-deps}\mbox{\isa{\isacommand{thms{\isacharunderscore}deps}}}^* & : & \isarkeep{theory~|~proof} \\
  10.114 -    \indexdef{}{command}{print-facts}\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}^* & : & \isarkeep{proof} \\
  10.115 -    \indexdef{}{command}{print-binds}\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}^* & : & \isarkeep{proof} \\
  10.116 +    \indexdef{}{command}{print\_commands}\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}^* & : & \isarkeep{\cdot} \\
  10.117 +    \indexdef{}{command}{print\_theory}\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}^* & : & \isarkeep{theory~|~proof} \\
  10.118 +    \indexdef{}{command}{print\_syntax}\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}^* & : & \isarkeep{theory~|~proof} \\
  10.119 +    \indexdef{}{command}{print\_methods}\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}^* & : & \isarkeep{theory~|~proof} \\
  10.120 +    \indexdef{}{command}{print\_attributes}\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}^* & : & \isarkeep{theory~|~proof} \\
  10.121 +    \indexdef{}{command}{print\_theorems}\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}^* & : & \isarkeep{theory~|~proof} \\
  10.122 +    \indexdef{}{command}{find\_theorems}\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}^* & : & \isarkeep{theory~|~proof} \\
  10.123 +    \indexdef{}{command}{thms\_deps}\mbox{\isa{\isacommand{thms{\isacharunderscore}deps}}}^* & : & \isarkeep{theory~|~proof} \\
  10.124 +    \indexdef{}{command}{print\_facts}\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}^* & : & \isarkeep{proof} \\
  10.125 +    \indexdef{}{command}{print\_binds}\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}^* & : & \isarkeep{proof} \\
  10.126    \end{matharray}
  10.127  
  10.128    \begin{rail}
  10.129 @@ -1745,9 +1745,9 @@
  10.130  \begin{matharray}{rcl}
  10.131      \indexdef{}{command}{cd}\mbox{\isa{\isacommand{cd}}}^* & : & \isarkeep{\cdot} \\
  10.132      \indexdef{}{command}{pwd}\mbox{\isa{\isacommand{pwd}}}^* & : & \isarkeep{\cdot} \\
  10.133 -    \indexdef{}{command}{use-thy}\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}^* & : & \isarkeep{\cdot} \\
  10.134 -    \indexdef{}{command}{display-drafts}\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}^* & : & \isarkeep{\cdot} \\
  10.135 -    \indexdef{}{command}{print-drafts}\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}^* & : & \isarkeep{\cdot} \\
  10.136 +    \indexdef{}{command}{use\_thy}\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}^* & : & \isarkeep{\cdot} \\
  10.137 +    \indexdef{}{command}{display\_drafts}\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}^* & : & \isarkeep{\cdot} \\
  10.138 +    \indexdef{}{command}{print\_drafts}\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}^* & : & \isarkeep{\cdot} \\
  10.139    \end{matharray}
  10.140  
  10.141    \begin{rail}

    11.1 --- a/doc-src/IsarRef/Thy/document/syntax.tex	Thu May 08 22:17:37 2008 +0200
    11.2 +++ b/doc-src/IsarRef/Thy/document/syntax.tex	Thu May 08 22:20:33 2008 +0200
    11.3 @@ -510,16 +510,16 @@
    11.4      \indexdef{}{antiquotation}{abbrev}\mbox{\isa{abbrev}} & : & \isarantiq \\
    11.5      \indexdef{}{antiquotation}{typeof}\mbox{\isa{typeof}} & : & \isarantiq \\
    11.6      \indexdef{}{antiquotation}{typ}\mbox{\isa{typ}} & : & \isarantiq \\
    11.7 -    \indexdef{}{antiquotation}{thm-style}\mbox{\isa{thm{\isacharunderscore}style}} & : & \isarantiq \\
    11.8 -    \indexdef{}{antiquotation}{term-style}\mbox{\isa{term{\isacharunderscore}style}} & : & \isarantiq \\
    11.9 +    \indexdef{}{antiquotation}{thm\_style}\mbox{\isa{thm{\isacharunderscore}style}} & : & \isarantiq \\
   11.10 +    \indexdef{}{antiquotation}{term\_style}\mbox{\isa{term{\isacharunderscore}style}} & : & \isarantiq \\
   11.11      \indexdef{}{antiquotation}{text}\mbox{\isa{text}} & : & \isarantiq \\
   11.12      \indexdef{}{antiquotation}{goals}\mbox{\isa{goals}} & : & \isarantiq \\
   11.13      \indexdef{}{antiquotation}{subgoals}\mbox{\isa{subgoals}} & : & \isarantiq \\
   11.14      \indexdef{}{antiquotation}{prf}\mbox{\isa{prf}} & : & \isarantiq \\
   11.15 -    \indexdef{}{antiquotation}{full-prf}\mbox{\isa{full{\isacharunderscore}prf}} & : & \isarantiq \\
   11.16 +    \indexdef{}{antiquotation}{full\_prf}\mbox{\isa{full{\isacharunderscore}prf}} & : & \isarantiq \\
   11.17      \indexdef{}{antiquotation}{ML}\mbox{\isa{ML}} & : & \isarantiq \\
   11.18 -    \indexdef{}{antiquotation}{ML-type}\mbox{\isa{ML{\isacharunderscore}type}} & : & \isarantiq \\
   11.19 -    \indexdef{}{antiquotation}{ML-struct}\mbox{\isa{ML{\isacharunderscore}struct}} & : & \isarantiq \\
   11.20 +    \indexdef{}{antiquotation}{ML\_type}\mbox{\isa{ML{\isacharunderscore}type}} & : & \isarantiq \\
   11.21 +    \indexdef{}{antiquotation}{ML\_struct}\mbox{\isa{ML{\isacharunderscore}struct}} & : & \isarantiq \\
   11.22    \end{matharray}
   11.23  
   11.24    The text body of formal comments (see also \secref{sec:comments})
   11.25 @@ -579,7 +579,7 @@
   11.26    \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints theorems
   11.27    \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}.  Note that attribute specifications
   11.28    may be included as well (see also \secref{sec:syn-att}); the
   11.29 -  \indexref{}{attribute}{no-vars}\mbox{\isa{no{\isacharunderscore}vars}} rule (see \secref{sec:misc-meth-att}) would
   11.30 +  \indexref{}{attribute}{no\_vars}\mbox{\isa{no{\isacharunderscore}vars}} rule (see \secref{sec:misc-meth-att}) would
   11.31    be particularly useful to suppress printing of schematic variables.
   11.32  
   11.33    \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.

    12.1 --- a/doc-src/IsarRef/isar-ref.tex	Thu May 08 22:17:37 2008 +0200
    12.2 +++ b/doc-src/IsarRef/isar-ref.tex	Thu May 08 22:20:33 2008 +0200
    12.3 @@ -4,6 +4,7 @@
    12.4  \documentclass[12pt,a4paper,fleqn]{report}
    12.5  \usepackage{latexsym,graphicx}
    12.6  \usepackage{../iman,../extra,../isar,../proof}
    12.7 +\usepackage[nohyphen,strings]{underscore}
    12.8  \usepackage{Thy/document/isabelle,Thy/document/isabellesym}
    12.9  \usepackage{../ttbox,,../rail,../railsetup}
   12.10  \usepackage{style}
   12.11 @@ -71,8 +72,6 @@
   12.12  
   12.13  \begin{document}
   12.14  
   12.15 -\underscoreoff
   12.16 -
   12.17  \maketitle 
   12.18  
   12.19  \pagenumbering{roman} \tableofcontents \clearfirst