--- a/doc-src/IsarImplementation/Thy/document/ML.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Thu May 08 22:20:33 2008 +0200
@@ -278,7 +278,7 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexml{NAMED-CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
+ \indexml{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
\indexml{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
\indexml{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
\end{mldecls}
@@ -487,7 +487,7 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
- \indexml{fold-map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
+ \indexml{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
\end{mldecls}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -622,12 +622,12 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexml{is-some}\verb|is_some: 'a option -> bool| \\
- \indexml{is-none}\verb|is_none: 'a option -> bool| \\
+ \indexml{is\_some}\verb|is_some: 'a option -> bool| \\
+ \indexml{is\_none}\verb|is_none: 'a option -> bool| \\
\indexml{the}\verb|the: 'a option -> 'a| \\
\indexml{these}\verb|these: 'a list option -> 'a list| \\
- \indexml{the-list}\verb|the_list: 'a option -> 'a list| \\
- \indexml{the-default}\verb|the_default: 'a -> 'a option -> 'a| \\
+ \indexml{the\_list}\verb|the_list: 'a option -> 'a list| \\
+ \indexml{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
\indexml{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
\indexml{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
\end{mldecls}%
@@ -699,9 +699,9 @@
\indexml{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
\indexml{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
\indexml{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
- \indexml{AList.map-entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
+ \indexml{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
\verb| -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list| \\
- \indexml{AList.map-default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
+ \indexml{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
\verb| -> ('a * 'b) list -> ('a * 'b) list| \\
\indexml{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline%
\verb| -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| \\
@@ -746,9 +746,9 @@
\indexml{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
\indexml{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
\verb| -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
- \indexml{Symtab.map-entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
+ \indexml{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
\verb| -> 'a Symtab.table -> 'a Symtab.table| \\
- \indexml{Symtab.map-default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
+ \indexml{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
\verb| -> 'a Symtab.table -> 'a Symtab.table| \\
\indexml{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
\verb| -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
--- a/doc-src/IsarImplementation/Thy/document/integration.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Thu May 08 22:20:33 2008 +0200
@@ -84,9 +84,9 @@
\begin{mldecls}
\indexmltype{Toplevel.state}\verb|type Toplevel.state| \\
\indexml{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
- \indexml{Toplevel.is-toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
- \indexml{Toplevel.theory-of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
- \indexml{Toplevel.proof-of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
+ \indexml{Toplevel.is\_toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
+ \indexml{Toplevel.theory\_of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
+ \indexml{Toplevel.proof\_of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
\indexml{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
\indexml{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
\indexml{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
@@ -173,18 +173,18 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
- \indexml{Toplevel.no-timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
+ \indexml{Toplevel.no\_timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
\indexml{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
\verb| Toplevel.transition -> Toplevel.transition| \\
\indexml{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
\verb| Toplevel.transition -> Toplevel.transition| \\
- \indexml{Toplevel.theory-to-proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
+ \indexml{Toplevel.theory\_to\_proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
\verb| Toplevel.transition -> Toplevel.transition| \\
\indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
\verb| Toplevel.transition -> Toplevel.transition| \\
\indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
\verb| Toplevel.transition -> Toplevel.transition| \\
- \indexml{Toplevel.end-proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
+ \indexml{Toplevel.end\_proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
\verb| Toplevel.transition -> Toplevel.transition| \\
\end{mldecls}
@@ -301,7 +301,7 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexml{the-context}\verb|the_context: unit -> theory| \\
+ \indexml{the\_context}\verb|the_context: unit -> theory| \\
\indexml{Context.$>$$>$ }\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
\end{mldecls}
@@ -436,15 +436,15 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexml{theory}\verb|theory: string -> theory| \\
- \indexml{use-thy}\verb|use_thy: string -> unit| \\
- \indexml{use-thys}\verb|use_thys: string list -> unit| \\
- \indexml{touch-thy}\verb|touch_thy: string -> unit| \\
- \indexml{remove-thy}\verb|remove_thy: string -> unit| \\[1ex]
- \indexml{ThyInfo.begin-theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
- \indexml{ThyInfo.end-theory}\verb|ThyInfo.end_theory: theory -> theory| \\
- \indexml{ThyInfo.register-theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
+ \indexml{use\_thy}\verb|use_thy: string -> unit| \\
+ \indexml{use\_thys}\verb|use_thys: string list -> unit| \\
+ \indexml{touch\_thy}\verb|touch_thy: string -> unit| \\
+ \indexml{remove\_thy}\verb|remove_thy: string -> unit| \\[1ex]
+ \indexml{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
+ \indexml{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> theory| \\
+ \indexml{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
\verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
- \indexml{ThyInfo.add-hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
+ \indexml{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
\end{mldecls}
\begin{description}
--- a/doc-src/IsarImplementation/Thy/document/logic.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Thu May 08 22:20:33 2008 +0200
@@ -132,18 +132,18 @@
\indexmltype{sort}\verb|type sort| \\
\indexmltype{arity}\verb|type arity| \\
\indexmltype{typ}\verb|type typ| \\
- \indexml{map-atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
- \indexml{fold-atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
+ \indexml{map\_atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
+ \indexml{fold\_atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
\end{mldecls}
\begin{mldecls}
\indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
- \indexml{Sign.of-sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
- \indexml{Sign.add-types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
- \indexml{Sign.add-tyabbrs-i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
+ \indexml{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
+ \indexml{Sign.add\_types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
+ \indexml{Sign.add\_tyabbrs\_i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
\verb| (string * string list * typ * mixfix) list -> theory -> theory| \\
- \indexml{Sign.primitive-class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
- \indexml{Sign.primitive-classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
- \indexml{Sign.primitive-arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
+ \indexml{Sign.primitive\_class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
+ \indexml{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
+ \indexml{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
\end{mldecls}
\begin{description}
@@ -319,21 +319,21 @@
\begin{mldecls}
\indexmltype{term}\verb|type term| \\
\indexml{op aconv}\verb|op aconv: term * term -> bool| \\
- \indexml{map-types}\verb|map_types: (typ -> typ) -> term -> term| \\
- \indexml{fold-types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
- \indexml{map-aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
- \indexml{fold-aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
+ \indexml{map\_types}\verb|map_types: (typ -> typ) -> term -> term| \\
+ \indexml{fold\_types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
+ \indexml{map\_aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
+ \indexml{fold\_aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
\end{mldecls}
\begin{mldecls}
- \indexml{fastype-of}\verb|fastype_of: term -> typ| \\
+ \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
\indexml{lambda}\verb|lambda: term -> term -> term| \\
\indexml{betapply}\verb|betapply: term * term -> term| \\
- \indexml{Sign.declare-const}\verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix ->|\isasep\isanewline%
+ \indexml{Sign.declare\_const}\verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix ->|\isasep\isanewline%
\verb| theory -> term * theory| \\
- \indexml{Sign.add-abbrev}\verb|Sign.add_abbrev: string -> Markup.property list -> bstring * term ->|\isasep\isanewline%
+ \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Markup.property list -> bstring * term ->|\isasep\isanewline%
\verb| theory -> (term * term) * theory| \\
- \indexml{Sign.const-typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
- \indexml{Sign.const-instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
+ \indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
+ \indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
\end{mldecls}
\begin{description}
@@ -579,27 +579,27 @@
\begin{mldecls}
\indexmltype{ctyp}\verb|type ctyp| \\
\indexmltype{cterm}\verb|type cterm| \\
- \indexml{Thm.ctyp-of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
- \indexml{Thm.cterm-of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
+ \indexml{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
+ \indexml{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
\end{mldecls}
\begin{mldecls}
\indexmltype{thm}\verb|type thm| \\
\indexml{proofs}\verb|proofs: int ref| \\
\indexml{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
- \indexml{Thm.forall-intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
- \indexml{Thm.forall-elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
- \indexml{Thm.implies-intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
- \indexml{Thm.implies-elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
+ \indexml{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
+ \indexml{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
+ \indexml{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
+ \indexml{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
\indexml{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
\indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
- \indexml{Thm.get-axiom-i}\verb|Thm.get_axiom_i: theory -> string -> thm| \\
- \indexml{Thm.invoke-oracle-i}\verb|Thm.invoke_oracle_i: theory -> string -> theory * Object.T -> thm| \\
+ \indexml{Thm.get\_axiom\_i}\verb|Thm.get_axiom_i: theory -> string -> thm| \\
+ \indexml{Thm.invoke\_oracle\_i}\verb|Thm.invoke_oracle_i: theory -> string -> theory * Object.T -> thm| \\
\end{mldecls}
\begin{mldecls}
- \indexml{Theory.add-axioms-i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\
- \indexml{Theory.add-deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
- \indexml{Theory.add-oracle}\verb|Theory.add_oracle: string * (theory * Object.T -> term) -> theory -> theory| \\
- \indexml{Theory.add-defs-i}\verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory| \\
+ \indexml{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\
+ \indexml{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
+ \indexml{Theory.add\_oracle}\verb|Theory.add_oracle: string * (theory * Object.T -> term) -> theory -> theory| \\
+ \indexml{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory| \\
\end{mldecls}
\begin{description}
@@ -739,10 +739,10 @@
\begin{mldecls}
\indexml{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\
\indexml{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\
- \indexml{Drule.mk-term}\verb|Drule.mk_term: cterm -> thm| \\
- \indexml{Drule.dest-term}\verb|Drule.dest_term: thm -> cterm| \\
- \indexml{Logic.mk-type}\verb|Logic.mk_type: typ -> term| \\
- \indexml{Logic.dest-type}\verb|Logic.dest_type: term -> typ| \\
+ \indexml{Drule.mk\_term}\verb|Drule.mk_term: cterm -> thm| \\
+ \indexml{Drule.dest\_term}\verb|Drule.dest_term: thm -> cterm| \\
+ \indexml{Logic.mk\_type}\verb|Logic.mk_type: typ -> term| \\
+ \indexml{Logic.dest\_type}\verb|Logic.dest_type: term -> typ| \\
\end{mldecls}
\begin{description}
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Thu May 08 22:20:33 2008 +0200
@@ -180,9 +180,9 @@
\indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\
\end{mldecls}
\begin{mldecls}
- \indexmltype{theory-ref}\verb|type theory_ref| \\
+ \indexmltype{theory\_ref}\verb|type theory_ref| \\
\indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
- \indexml{Theory.check-thy}\verb|Theory.check_thy: theory -> theory_ref| \\
+ \indexml{Theory.check\_thy}\verb|Theory.check_thy: theory -> theory_ref| \\
\end{mldecls}
\begin{description}
@@ -276,7 +276,7 @@
\begin{mldecls}
\indexmltype{Proof.context}\verb|type Proof.context| \\
\indexml{ProofContext.init}\verb|ProofContext.init: theory -> Proof.context| \\
- \indexml{ProofContext.theory-of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
+ \indexml{ProofContext.theory\_of}\verb|ProofContext.theory_of: Proof.context -> theory| \\
\indexml{ProofContext.transfer}\verb|ProofContext.transfer: theory -> Proof.context -> Proof.context| \\
\end{mldecls}
@@ -334,8 +334,8 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{Context.generic}\verb|type Context.generic| \\
- \indexml{Context.theory-of}\verb|Context.theory_of: Context.generic -> theory| \\
- \indexml{Context.proof-of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
+ \indexml{Context.theory\_of}\verb|Context.theory_of: Context.generic -> theory| \\
+ \indexml{Context.proof\_of}\verb|Context.proof_of: Context.generic -> Proof.context| \\
\end{mldecls}
\begin{description}
@@ -553,10 +553,10 @@
\begin{mldecls}
\indexmltype{Symbol.symbol}\verb|type Symbol.symbol| \\
\indexml{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
- \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
- \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
- \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
- \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
+ \indexml{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
+ \indexml{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
+ \indexml{Symbol.is\_quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
+ \indexml{Symbol.is\_blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
\end{mldecls}
\begin{mldecls}
\indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
@@ -814,8 +814,8 @@
\end{mldecls}
\begin{mldecls}
\indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
- \indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
- \indexml{NameSpace.add-path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
+ \indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
+ \indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
\indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\
\end{mldecls}
\begin{mldecls}
--- a/doc-src/IsarImplementation/Thy/document/proof.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Thu May 08 22:20:33 2008 +0200
@@ -104,15 +104,15 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexml{Variable.add-fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
+ \indexml{Variable.add\_fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
\verb| string list -> Proof.context -> string list * Proof.context| \\
- \indexml{Variable.variant-fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
+ \indexml{Variable.variant\_fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
\verb| string list -> Proof.context -> string list * Proof.context| \\
- \indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
- \indexml{Variable.declare-constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
+ \indexml{Variable.declare\_term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
+ \indexml{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
\indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
\indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
- \indexml{Variable.import-thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
+ \indexml{Variable.import\_thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
\verb| ((ctyp list * cterm list) * thm list) * Proof.context| \\
\indexml{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
\end{mldecls}
@@ -235,9 +235,9 @@
\begin{mldecls}
\indexmltype{Assumption.export}\verb|type Assumption.export| \\
\indexml{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
- \indexml{Assumption.add-assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
+ \indexml{Assumption.add\_assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
\verb| cterm list -> Proof.context -> thm list * Proof.context| \\
- \indexml{Assumption.add-assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
+ \indexml{Assumption.add\_assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
\verb| cterm list -> Proof.context -> thm list * Proof.context| \\
\indexml{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
\end{mldecls}
@@ -333,7 +333,7 @@
\begin{mldecls}
\indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
- \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
+ \indexml{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
\end{mldecls}
\begin{mldecls}
--- a/doc-src/IsarImplementation/implementation.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarImplementation/implementation.tex Thu May 08 22:20:33 2008 +0200
@@ -5,6 +5,7 @@
\usepackage{latexsym,graphicx}
\usepackage[refpage]{nomencl}
\usepackage{../iman,../extra,../isar,../proof}
+\usepackage[nohyphen,strings]{underscore}
\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
\usepackage{style}
\usepackage{../pdfsetup}
--- a/doc-src/IsarRef/Thy/document/Generic.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Thu May 08 22:20:33 2008 +0200
@@ -38,9 +38,9 @@
\indexdef{}{command}{definition}\mbox{\isa{\isacommand{definition}}} & : & \isarkeep{local{\dsh}theory} \\
\indexdef{}{attribute}{defn}\mbox{\isa{defn}} & : & \isaratt \\
\indexdef{}{command}{abbreviation}\mbox{\isa{\isacommand{abbreviation}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{print-abbrevs}\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_abbrevs}\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{command}{notation}\mbox{\isa{\isacommand{notation}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{no-notation}\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{no\_notation}\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}} & : & \isarkeep{local{\dsh}theory} \\
\end{matharray}
These specification mechanisms provide a slightly more abstract view
@@ -256,10 +256,10 @@
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{locale}\mbox{\isa{\isacommand{locale}}} & : & \isartrans{theory}{local{\dsh}theory} \\
- \indexdef{}{command}{print-locale}\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{command}{print-locales}\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{method}{intro-locales}\mbox{\isa{intro{\isacharunderscore}locales}} & : & \isarmeth \\
- \indexdef{}{method}{unfold-locales}\mbox{\isa{unfold{\isacharunderscore}locales}} & : & \isarmeth \\
+ \indexdef{}{command}{print\_locale}\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_locales}\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{method}{intro\_locales}\mbox{\isa{intro{\isacharunderscore}locales}} & : & \isarmeth \\
+ \indexdef{}{method}{unfold\_locales}\mbox{\isa{unfold{\isacharunderscore}locales}} & : & \isarmeth \\
\end{matharray}
\indexouternonterm{contextexpr}\indexouternonterm{contextelem}
@@ -421,7 +421,7 @@
\begin{matharray}{rcl}
\indexdef{}{command}{interpretation}\mbox{\isa{\isacommand{interpretation}}} & : & \isartrans{theory}{proof(prove)} \\
\indexdef{}{command}{interpret}\mbox{\isa{\isacommand{interpret}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
- \indexdef{}{command}{print-interps}\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_interps}\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\end{matharray}
\indexouternonterm{interp}
@@ -560,8 +560,8 @@
\indexdef{}{command}{instantiation}\mbox{\isa{\isacommand{instantiation}}} & : & \isartrans{theory}{local{\dsh}theory} \\
\indexdef{}{command}{instance}\mbox{\isa{\isacommand{instance}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
\indexdef{}{command}{subclass}\mbox{\isa{\isacommand{subclass}}} & : & \isartrans{local{\dsh}theory}{local{\dsh}theory} \\
- \indexdef{}{command}{print-classes}\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{method}{intro-classes}\mbox{\isa{intro{\isacharunderscore}classes}} & : & \isarmeth \\
+ \indexdef{}{command}{print\_classes}\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{method}{intro\_classes}\mbox{\isa{intro{\isacharunderscore}classes}} & : & \isarmeth \\
\end{matharray}
\begin{rail}
@@ -769,7 +769,7 @@
``global'', which may not be changed within a local context.
\begin{matharray}{rcll}
- \indexdef{}{command}{print-configs}\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_configs}\mbox{\isa{\isacommand{print{\isacharunderscore}configs}}} & : & \isarkeep{theory~|~proof} \\
\end{matharray}
\begin{rail}
@@ -881,7 +881,7 @@
\indexdef{}{command}{finally}\mbox{\isa{\isacommand{finally}}} & : & \isartrans{proof(state)}{proof(chain)} \\
\indexdef{}{command}{moreover}\mbox{\isa{\isacommand{moreover}}} & : & \isartrans{proof(state)}{proof(state)} \\
\indexdef{}{command}{ultimately}\mbox{\isa{\isacommand{ultimately}}} & : & \isartrans{proof(state)}{proof(chain)} \\
- \indexdef{}{command}{print-trans-rules}\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_trans\_rules}\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\mbox{\isa{trans}} & : & \isaratt \\
\mbox{\isa{sym}} & : & \isaratt \\
\mbox{\isa{symmetric}} & : & \isaratt \\
@@ -1045,9 +1045,9 @@
\indexdef{}{attribute}{unfolded}\mbox{\isa{unfolded}} & : & \isaratt \\
\indexdef{}{attribute}{folded}\mbox{\isa{folded}} & : & \isaratt \\[0.5ex]
\indexdef{}{attribute}{rotated}\mbox{\isa{rotated}} & : & \isaratt \\
- \indexdef{Pure}{attribute}{elim-format}\mbox{\isa{elim{\isacharunderscore}format}} & : & \isaratt \\
+ \indexdef{Pure}{attribute}{elim\_format}\mbox{\isa{elim{\isacharunderscore}format}} & : & \isaratt \\
\indexdef{}{attribute}{standard}\mbox{\isa{standard}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
- \indexdef{}{attribute}{no-vars}\mbox{\isa{no{\isacharunderscore}vars}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
+ \indexdef{}{attribute}{no\_vars}\mbox{\isa{no{\isacharunderscore}vars}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
\end{matharray}
\begin{rail}
@@ -1135,15 +1135,15 @@
\secref{sec:pure-meth-att}).
\begin{matharray}{rcl}
- \indexdef{}{method}{rule-tac}\mbox{\isa{rule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{}{method}{erule-tac}\mbox{\isa{erule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{}{method}{drule-tac}\mbox{\isa{drule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{}{method}{frule-tac}\mbox{\isa{frule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{}{method}{cut-tac}\mbox{\isa{cut{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{}{method}{thin-tac}\mbox{\isa{thin{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{}{method}{subgoal-tac}\mbox{\isa{subgoal{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{}{method}{rename-tac}\mbox{\isa{rename{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{}{method}{rotate-tac}\mbox{\isa{rotate{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{}{method}{rule\_tac}\mbox{\isa{rule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{}{method}{erule\_tac}\mbox{\isa{erule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{}{method}{drule\_tac}\mbox{\isa{drule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{}{method}{frule\_tac}\mbox{\isa{frule{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{}{method}{cut\_tac}\mbox{\isa{cut{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{}{method}{thin\_tac}\mbox{\isa{thin{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{}{method}{subgoal\_tac}\mbox{\isa{subgoal{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{}{method}{rename\_tac}\mbox{\isa{rename{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{}{method}{rotate\_tac}\mbox{\isa{rotate{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
\indexdef{}{method}{tactic}\mbox{\isa{tactic}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
\end{matharray}
@@ -1227,7 +1227,7 @@
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{method}{simp}\mbox{\isa{simp}} & : & \isarmeth \\
- \indexdef{}{method}{simp-all}\mbox{\isa{simp{\isacharunderscore}all}} & : & \isarmeth \\
+ \indexdef{}{method}{simp\_all}\mbox{\isa{simp{\isacharunderscore}all}} & : & \isarmeth \\
\end{matharray}
\indexouternonterm{simpmod}
@@ -1301,7 +1301,7 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{}{command}{print-simpset}\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_simpset}\mbox{\isa{\isacommand{print{\isacharunderscore}simpset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{attribute}{simp}\mbox{\isa{simp}} & : & \isaratt \\
\indexdef{}{attribute}{cong}\mbox{\isa{cong}} & : & \isaratt \\
\indexdef{}{attribute}{split}\mbox{\isa{split}} & : & \isaratt \\
@@ -1334,7 +1334,7 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{}{command}{simproc-setup}\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{simproc\_setup}\mbox{\isa{\isacommand{simproc{\isacharunderscore}setup}}} & : & \isarkeep{local{\dsh}theory} \\
simproc & : & \isaratt \\
\end{matharray}
@@ -1621,7 +1621,7 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{}{command}{print-claset}\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_claset}\mbox{\isa{\isacommand{print{\isacharunderscore}claset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{attribute}{intro}\mbox{\isa{intro}} & : & \isaratt \\
\indexdef{}{attribute}{elim}\mbox{\isa{elim}} & : & \isaratt \\
\indexdef{}{attribute}{dest}\mbox{\isa{dest}} & : & \isaratt \\
@@ -1700,9 +1700,9 @@
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{case}\mbox{\isa{\isacommand{case}}} & : & \isartrans{proof(state)}{proof(state)} \\
- \indexdef{}{command}{print-cases}\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
- \indexdef{}{attribute}{case-names}\mbox{\isa{case{\isacharunderscore}names}} & : & \isaratt \\
- \indexdef{}{attribute}{case-conclusion}\mbox{\isa{case{\isacharunderscore}conclusion}} & : & \isaratt \\
+ \indexdef{}{command}{print\_cases}\mbox{\isa{\isacommand{print{\isacharunderscore}cases}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
+ \indexdef{}{attribute}{case\_names}\mbox{\isa{case{\isacharunderscore}names}} & : & \isaratt \\
+ \indexdef{}{attribute}{case\_conclusion}\mbox{\isa{case{\isacharunderscore}conclusion}} & : & \isaratt \\
\indexdef{}{attribute}{params}\mbox{\isa{params}} & : & \isaratt \\
\indexdef{}{attribute}{consumes}\mbox{\isa{consumes}} & : & \isaratt \\
\end{matharray}
@@ -2000,7 +2000,7 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{}{command}{print-induct-rules}\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_induct\_rules}\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{}{attribute}{cases}\mbox{\isa{cases}} & : & \isaratt \\
\indexdef{}{attribute}{induct}\mbox{\isa{induct}} & : & \isaratt \\
\indexdef{}{attribute}{coinduct}\mbox{\isa{coinduct}} & : & \isaratt \\
@@ -2047,7 +2047,7 @@
\indexdef{}{command}{judgment}\mbox{\isa{\isacommand{judgment}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{method}{atomize}\mbox{\isa{atomize}} & : & \isarmeth \\
\indexdef{}{attribute}{atomize}\mbox{\isa{atomize}} & : & \isaratt \\
- \indexdef{}{attribute}{rule-format}\mbox{\isa{rule{\isacharunderscore}format}} & : & \isaratt \\
+ \indexdef{}{attribute}{rule\_format}\mbox{\isa{rule{\isacharunderscore}format}} & : & \isaratt \\
\indexdef{}{attribute}{rulify}\mbox{\isa{rulify}} & : & \isaratt \\
\end{matharray}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 08 22:20:33 2008 +0200
@@ -364,7 +364,7 @@
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{HOL}{command}{datatype}\mbox{\isa{\isacommand{datatype}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{rep-datatype}\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{rep\_datatype}\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}
@@ -517,9 +517,9 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{HOL}{method}{pat-completeness}\mbox{\isa{pat{\isacharunderscore}completeness}} & : & \isarmeth \\
+ \indexdef{HOL}{method}{pat\_completeness}\mbox{\isa{pat{\isacharunderscore}completeness}} & : & \isarmeth \\
\indexdef{HOL}{method}{relation}\mbox{\isa{relation}} & : & \isarmeth \\
- \indexdef{HOL}{method}{lexicographic-order}\mbox{\isa{lexicographic{\isacharunderscore}order}} & : & \isarmeth \\
+ \indexdef{HOL}{method}{lexicographic\_order}\mbox{\isa{lexicographic{\isacharunderscore}order}} & : & \isarmeth \\
\end{matharray}
\begin{rail}
@@ -567,7 +567,7 @@
\begin{matharray}{rcl}
\indexdef{HOL}{command}{recdef}\mbox{\isa{\isacommand{recdef}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{recdef-tc}\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\
+ \indexdef{HOL}{command}{recdef\_tc}\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\
\end{matharray}
\begin{rail}
@@ -609,9 +609,9 @@
globally, using the following attributes.
\begin{matharray}{rcl}
- \indexdef{HOL}{attribute}{recdef-simp}\mbox{\isa{recdef{\isacharunderscore}simp}} & : & \isaratt \\
- \indexdef{HOL}{attribute}{recdef-cong}\mbox{\isa{recdef{\isacharunderscore}cong}} & : & \isaratt \\
- \indexdef{HOL}{attribute}{recdef-wf}\mbox{\isa{recdef{\isacharunderscore}wf}} & : & \isaratt \\
+ \indexdef{HOL}{attribute}{recdef\_simp}\mbox{\isa{recdef{\isacharunderscore}simp}} & : & \isaratt \\
+ \indexdef{HOL}{attribute}{recdef\_cong}\mbox{\isa{recdef{\isacharunderscore}cong}} & : & \isaratt \\
+ \indexdef{HOL}{attribute}{recdef\_wf}\mbox{\isa{recdef{\isacharunderscore}wf}} & : & \isaratt \\
\end{matharray}
\begin{rail}
@@ -628,7 +628,7 @@
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{HOL}{command}{specification}\mbox{\isa{\isacommand{specification}}} & : & \isartrans{theory}{proof(prove)} \\
- \indexdef{HOL}{command}{ax-specification}\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} & : & \isartrans{theory}{proof(prove)} \\
+ \indexdef{HOL}{command}{ax\_specification}\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} & : & \isartrans{theory}{proof(prove)} \\
\end{matharray}
\begin{rail}
@@ -698,9 +698,9 @@
\begin{matharray}{rcl}
\indexdef{HOL}{command}{inductive}\mbox{\isa{\isacommand{inductive}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{HOL}{command}{inductive-set}\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{HOL}{command}{inductive\_set}\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
\indexdef{HOL}{command}{coinductive}\mbox{\isa{\isacommand{coinductive}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{HOL}{command}{coinductive-set}\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{HOL}{command}{coinductive\_set}\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
\indexdef{HOL}{attribute}{mono}\mbox{\isa{mono}} & : & \isaratt \\
\end{matharray}
@@ -817,7 +817,7 @@
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{HOL}{method}{arith}\mbox{\isa{arith}} & : & \isarmeth \\
- \indexdef{HOL}{method}{arith-split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
+ \indexdef{HOL}{method}{arith\_split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
\end{matharray}
The \mbox{\isa{arith}} method decides linear arithmetic problems
@@ -841,10 +841,10 @@
ported to Isar. These should be never used in proper proof texts!
\begin{matharray}{rcl}
- \indexdef{HOL}{method}{case-tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{HOL}{method}{induct-tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{HOL}{method}{ind-cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{HOL}{command}{inductive-cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{method}{case\_tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{HOL}{method}{induct\_tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{HOL}{method}{ind\_cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{HOL}{command}{inductive\_cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}
@@ -900,10 +900,10 @@
\begin{matharray}{rcl}
\indexdef{HOL}{command}{value}\mbox{\isa{\isacommand{value}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \indexdef{HOL}{command}{code-module}\mbox{\isa{\isacommand{code{\isacharunderscore}module}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{code-library}\mbox{\isa{\isacommand{code{\isacharunderscore}library}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{consts-code}\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{types-code}\mbox{\isa{\isacommand{types{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{code\_module}\mbox{\isa{\isacommand{code{\isacharunderscore}module}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{code\_library}\mbox{\isa{\isacommand{code{\isacharunderscore}library}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{consts\_code}\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{types\_code}\mbox{\isa{\isacommand{types{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\
\indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\
\end{matharray}
@@ -961,20 +961,20 @@
introduction on how to use it.
\begin{matharray}{rcl}
- \indexdef{HOL}{command}{export-code}\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \indexdef{HOL}{command}{code-thms}\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \indexdef{HOL}{command}{code-deps}\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \indexdef{HOL}{command}{code-datatype}\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{code-const}\mbox{\isa{\isacommand{code{\isacharunderscore}const}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{code-type}\mbox{\isa{\isacommand{code{\isacharunderscore}type}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{code-class}\mbox{\isa{\isacommand{code{\isacharunderscore}class}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{code-instance}\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{code-monad}\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{code-reserved}\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{code-include}\mbox{\isa{\isacommand{code{\isacharunderscore}include}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{code-modulename}\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{code-exception}\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}} & : & \isartrans{theory}{theory} \\
- \indexdef{HOL}{command}{print-codesetup}\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{HOL}{command}{export\_code}\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{HOL}{command}{code\_thms}\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{HOL}{command}{code\_deps}\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{HOL}{command}{code\_datatype}\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{code\_const}\mbox{\isa{\isacommand{code{\isacharunderscore}const}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{code\_type}\mbox{\isa{\isacommand{code{\isacharunderscore}type}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{code\_class}\mbox{\isa{\isacommand{code{\isacharunderscore}class}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{code\_instance}\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{code\_monad}\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{code\_reserved}\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{code\_include}\mbox{\isa{\isacommand{code{\isacharunderscore}include}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{code\_modulename}\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{code\_exception}\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOL}{command}{print\_codesetup}\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\
\end{matharray}
--- a/doc-src/IsarRef/Thy/document/ZF_Specific.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/ZF_Specific.tex Thu May 08 22:20:33 2008 +0200
@@ -36,7 +36,7 @@
Simplifier setup.
\begin{matharray}{rcl}
- \indexdef{ZF}{command}{print-tcset}\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{ZF}{command}{print\_tcset}\mbox{\isa{\isacommand{print{\isacharunderscore}tcset}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
\indexdef{ZF}{method}{typecheck}\mbox{\isa{typecheck}} & : & \isarmeth \\
\indexdef{ZF}{attribute}{TC}\mbox{\isa{TC}} & : & \isaratt \\
\end{matharray}
@@ -148,10 +148,10 @@
ported to Isar. These should not be used in proper proof texts.
\begin{matharray}{rcl}
- \indexdef{ZF}{method}{case-tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{ZF}{method}{induct-tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{ZF}{method}{ind-cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{ZF}{command}{inductive-cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{ZF}{method}{case\_tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{ZF}{method}{induct\_tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{ZF}{method}{ind\_cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+ \indexdef{ZF}{command}{inductive\_cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}
--- a/doc-src/IsarRef/Thy/document/pure.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/pure.tex Thu May 08 22:20:33 2008 +0200
@@ -128,7 +128,7 @@
\indexdef{}{command}{subsection}\mbox{\isa{\isacommand{subsection}}} & : & \isarkeep{local{\dsh}theory} \\
\indexdef{}{command}{subsubsection}\mbox{\isa{\isacommand{subsubsection}}} & : & \isarkeep{local{\dsh}theory} \\
\indexdef{}{command}{text}\mbox{\isa{\isacommand{text}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{text-raw}\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}} & : & \isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{text\_raw}\mbox{\isa{\isacommand{text{\isacharunderscore}raw}}} & : & \isarkeep{local{\dsh}theory} \\
\end{matharray}
Apart from formal comments (see \secref{sec:comments}), markup
@@ -184,7 +184,7 @@
\indexdef{}{command}{classes}\mbox{\isa{\isacommand{classes}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{classrel}\mbox{\isa{\isacommand{classrel}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
\indexdef{}{command}{defaultsort}\mbox{\isa{\isacommand{defaultsort}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{class-deps}\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}} & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{class\_deps}\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}} & : & \isarkeep{theory~|~proof} \\
\end{matharray}
\begin{rail}
@@ -380,9 +380,9 @@
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{command}{syntax}\mbox{\isa{\isacommand{syntax}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{no-syntax}\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{no\_syntax}\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}} & : & \isartrans{theory}{theory} \\
\indexdef{}{command}{translations}\mbox{\isa{\isacommand{translations}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{no-translations}\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{no\_translations}\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}
@@ -521,10 +521,10 @@
\begin{matharray}{rcl}
\indexdef{}{command}{use}\mbox{\isa{\isacommand{use}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
\indexdef{}{command}{ML}\mbox{\isa{\isacommand{ML}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
- \indexdef{}{command}{ML-val}\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}} & : & \isartrans{\cdot}{\cdot} \\
- \indexdef{}{command}{ML-command}\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}} & : & \isartrans{\cdot}{\cdot} \\
+ \indexdef{}{command}{ML\_val}\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}} & : & \isartrans{\cdot}{\cdot} \\
+ \indexdef{}{command}{ML\_command}\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}} & : & \isartrans{\cdot}{\cdot} \\
\indexdef{}{command}{setup}\mbox{\isa{\isacommand{setup}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{method-setup}\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{method\_setup}\mbox{\isa{\isacommand{method{\isacharunderscore}setup}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}
@@ -591,12 +591,12 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{}{command}{parse-ast-translation}\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{parse-translation}\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{print-translation}\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{typed-print-translation}\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{print-ast-translation}\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
- \indexdef{}{command}{token-translation}\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{parse\_ast\_translation}\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{parse\_translation}\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{print\_translation}\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{typed\_print\_translation}\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{print\_ast\_translation}\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{}{command}{token\_translation}\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}
@@ -734,7 +734,7 @@
\indexdef{}{command}{subsect}\mbox{\isa{\isacommand{subsect}}} & : & \isartrans{proof}{proof} \\
\indexdef{}{command}{subsubsect}\mbox{\isa{\isacommand{subsubsect}}} & : & \isartrans{proof}{proof} \\
\indexdef{}{command}{txt}\mbox{\isa{\isacommand{txt}}} & : & \isartrans{proof}{proof} \\
- \indexdef{}{command}{txt-raw}\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}} & : & \isartrans{proof}{proof} \\
+ \indexdef{}{command}{txt\_raw}\mbox{\isa{\isacommand{txt{\isacharunderscore}raw}}} & : & \isartrans{proof}{proof} \\
\end{matharray}
These markup commands for proof mode closely correspond to the ones
@@ -905,7 +905,7 @@
of the premises of the rule involved. Note that positions may be
easily skipped using something like \mbox{\isa{\isacommand{from}}}~\isa{{\isachardoublequote}{\isacharunderscore}\ {\isasymAND}\ a\ {\isasymAND}\ b{\isachardoublequote}}, for example. This involves the trivial rule
\isa{{\isachardoublequote}PROP\ {\isasympsi}\ {\isasymLongrightarrow}\ PROP\ {\isasympsi}{\isachardoublequote}}, which is bound in Isabelle/Pure as
- ``\indexref{}{fact}{-}\mbox{\isa{{\isacharunderscore}}}'' (underscore).
+ ``\indexref{}{fact}{\_}\mbox{\isa{{\isacharunderscore}}}'' (underscore).
Automated methods (such as \mbox{\isa{simp}} or \mbox{\isa{auto}}) just
insert any given facts before their usual operation. Depending on
@@ -1032,7 +1032,7 @@
Any goal statement causes some term abbreviations (such as
\indexref{}{variable}{?thesis}\mbox{\isa{{\isacharquery}thesis}}) to be bound automatically, see also
\secref{sec:term-abbrev}. Furthermore, the local context of a
- (non-atomic) goal is provided via the \indexref{}{case}{rule-context}\mbox{\isa{rule{\isacharunderscore}context}} case.
+ (non-atomic) goal is provided via the \indexref{}{case}{rule\_context}\mbox{\isa{rule{\isacharunderscore}context}} case.
The optional case names of \indexref{}{element}{obtains}\mbox{\isa{\isakeyword{obtains}}} have a twofold
meaning: (1) during the of this claim they refer to the the local
@@ -1430,7 +1430,7 @@
\begin{matharray}{rcl}
\indexdef{}{command}{apply}\mbox{\isa{\isacommand{apply}}}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
- \indexdef{}{command}{apply-end}\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}^* & : & \isartrans{proof(state)}{proof(state)} \\
+ \indexdef{}{command}{apply\_end}\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}^* & : & \isartrans{proof(state)}{proof(state)} \\
\indexdef{}{command}{done}\mbox{\isa{\isacommand{done}}}^* & : & \isartrans{proof(prove)}{proof(state)} \\
\indexdef{}{command}{defer}\mbox{\isa{\isacommand{defer}}}^* & : & \isartrans{proof}{proof} \\
\indexdef{}{command}{prefer}\mbox{\isa{\isacommand{prefer}}}^* & : & \isartrans{proof}{proof} \\
@@ -1621,16 +1621,16 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{}{command}{print-commands}\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}^* & : & \isarkeep{\cdot} \\
- \indexdef{}{command}{print-theory}\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}^* & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{command}{print-syntax}\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}^* & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{command}{print-methods}\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}^* & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{command}{print-attributes}\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}^* & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{command}{print-theorems}\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}^* & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{command}{find-theorems}\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}^* & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{command}{thms-deps}\mbox{\isa{\isacommand{thms{\isacharunderscore}deps}}}^* & : & \isarkeep{theory~|~proof} \\
- \indexdef{}{command}{print-facts}\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}^* & : & \isarkeep{proof} \\
- \indexdef{}{command}{print-binds}\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}^* & : & \isarkeep{proof} \\
+ \indexdef{}{command}{print\_commands}\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}^* & : & \isarkeep{\cdot} \\
+ \indexdef{}{command}{print\_theory}\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_syntax}\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_methods}\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_attributes}\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_theorems}\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{find\_theorems}\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{thms\_deps}\mbox{\isa{\isacommand{thms{\isacharunderscore}deps}}}^* & : & \isarkeep{theory~|~proof} \\
+ \indexdef{}{command}{print\_facts}\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}^* & : & \isarkeep{proof} \\
+ \indexdef{}{command}{print\_binds}\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}^* & : & \isarkeep{proof} \\
\end{matharray}
\begin{rail}
@@ -1745,9 +1745,9 @@
\begin{matharray}{rcl}
\indexdef{}{command}{cd}\mbox{\isa{\isacommand{cd}}}^* & : & \isarkeep{\cdot} \\
\indexdef{}{command}{pwd}\mbox{\isa{\isacommand{pwd}}}^* & : & \isarkeep{\cdot} \\
- \indexdef{}{command}{use-thy}\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}^* & : & \isarkeep{\cdot} \\
- \indexdef{}{command}{display-drafts}\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}^* & : & \isarkeep{\cdot} \\
- \indexdef{}{command}{print-drafts}\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}^* & : & \isarkeep{\cdot} \\
+ \indexdef{}{command}{use\_thy}\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}^* & : & \isarkeep{\cdot} \\
+ \indexdef{}{command}{display\_drafts}\mbox{\isa{\isacommand{display{\isacharunderscore}drafts}}}^* & : & \isarkeep{\cdot} \\
+ \indexdef{}{command}{print\_drafts}\mbox{\isa{\isacommand{print{\isacharunderscore}drafts}}}^* & : & \isarkeep{\cdot} \\
\end{matharray}
\begin{rail}
--- a/doc-src/IsarRef/Thy/document/syntax.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/syntax.tex Thu May 08 22:20:33 2008 +0200
@@ -510,16 +510,16 @@
\indexdef{}{antiquotation}{abbrev}\mbox{\isa{abbrev}} & : & \isarantiq \\
\indexdef{}{antiquotation}{typeof}\mbox{\isa{typeof}} & : & \isarantiq \\
\indexdef{}{antiquotation}{typ}\mbox{\isa{typ}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{thm-style}\mbox{\isa{thm{\isacharunderscore}style}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{term-style}\mbox{\isa{term{\isacharunderscore}style}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{thm\_style}\mbox{\isa{thm{\isacharunderscore}style}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{term\_style}\mbox{\isa{term{\isacharunderscore}style}} & : & \isarantiq \\
\indexdef{}{antiquotation}{text}\mbox{\isa{text}} & : & \isarantiq \\
\indexdef{}{antiquotation}{goals}\mbox{\isa{goals}} & : & \isarantiq \\
\indexdef{}{antiquotation}{subgoals}\mbox{\isa{subgoals}} & : & \isarantiq \\
\indexdef{}{antiquotation}{prf}\mbox{\isa{prf}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{full-prf}\mbox{\isa{full{\isacharunderscore}prf}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{full\_prf}\mbox{\isa{full{\isacharunderscore}prf}} & : & \isarantiq \\
\indexdef{}{antiquotation}{ML}\mbox{\isa{ML}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{ML-type}\mbox{\isa{ML{\isacharunderscore}type}} & : & \isarantiq \\
- \indexdef{}{antiquotation}{ML-struct}\mbox{\isa{ML{\isacharunderscore}struct}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{ML\_type}\mbox{\isa{ML{\isacharunderscore}type}} & : & \isarantiq \\
+ \indexdef{}{antiquotation}{ML\_struct}\mbox{\isa{ML{\isacharunderscore}struct}} & : & \isarantiq \\
\end{matharray}
The text body of formal comments (see also \secref{sec:comments})
@@ -579,7 +579,7 @@
\item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharbraceright}{\isachardoublequote}}] prints theorems
\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}. Note that attribute specifications
may be included as well (see also \secref{sec:syn-att}); the
- \indexref{}{attribute}{no-vars}\mbox{\isa{no{\isacharunderscore}vars}} rule (see \secref{sec:misc-meth-att}) would
+ \indexref{}{attribute}{no\_vars}\mbox{\isa{no{\isacharunderscore}vars}} rule (see \secref{sec:misc-meth-att}) would
be particularly useful to suppress printing of schematic variables.
\item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
--- a/doc-src/IsarRef/isar-ref.tex Thu May 08 22:17:37 2008 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Thu May 08 22:20:33 2008 +0200
@@ -4,6 +4,7 @@
\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{latexsym,graphicx}
\usepackage{../iman,../extra,../isar,../proof}
+\usepackage[nohyphen,strings]{underscore}
\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
\usepackage{../ttbox,,../rail,../railsetup}
\usepackage{style}
@@ -71,8 +72,6 @@
\begin{document}
-\underscoreoff
-
\maketitle
\pagenumbering{roman} \tableofcontents \clearfirst