# HG changeset patch # User wenzelm # Date 1621713133 -7200 # Node ID 35d8132633c65250e15c7ac080969500fc22db35 # Parent eccc4a13216d1f6a73ca56c5935822257b02a650 clarified names; diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Eq.thy --- a/src/Doc/Implementation/Eq.thy Sat May 22 13:35:25 2021 +0200 +++ b/src/Doc/Implementation/Eq.thy Sat May 22 21:52:13 2021 +0200 @@ -55,13 +55,13 @@ text %mlref \ \begin{mldecls} - @{index_ML Thm.reflexive: "cterm -> thm"} \\ - @{index_ML Thm.symmetric: "thm -> thm"} \\ - @{index_ML Thm.transitive: "thm -> thm -> thm"} \\ - @{index_ML Thm.abstract_rule: "string -> cterm -> thm -> thm"} \\ - @{index_ML Thm.combination: "thm -> thm -> thm"} \\[0.5ex] - @{index_ML Thm.equal_intr: "thm -> thm -> thm"} \\ - @{index_ML Thm.equal_elim: "thm -> thm -> thm"} \\ + @{define_ML Thm.reflexive: "cterm -> thm"} \\ + @{define_ML Thm.symmetric: "thm -> thm"} \\ + @{define_ML Thm.transitive: "thm -> thm -> thm"} \\ + @{define_ML Thm.abstract_rule: "string -> cterm -> thm -> thm"} \\ + @{define_ML Thm.combination: "thm -> thm -> thm"} \\[0.5ex] + @{define_ML Thm.equal_intr: "thm -> thm -> thm"} \\ + @{define_ML Thm.equal_elim: "thm -> thm -> thm"} \\ \end{mldecls} See also \<^file>\~~/src/Pure/thm.ML\ for further description of these inference @@ -82,9 +82,9 @@ text %mlref \ \begin{mldecls} - @{index_ML_structure Conv} \\ - @{index_ML_type conv} \\ - @{index_ML Simplifier.asm_full_rewrite : "Proof.context -> conv"} \\ + @{define_ML_structure Conv} \\ + @{define_ML_type conv} \\ + @{define_ML Simplifier.asm_full_rewrite : "Proof.context -> conv"} \\ \end{mldecls} \<^descr> \<^ML_structure>\Conv\ is a library of combinators to build conversions, @@ -109,11 +109,11 @@ text %mlref \ \begin{mldecls} - @{index_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\ - @{index_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\ - @{index_ML rewrite_goal_tac: "Proof.context -> thm list -> int -> tactic"} \\ - @{index_ML rewrite_goals_tac: "Proof.context -> thm list -> tactic"} \\ - @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\ + @{define_ML rewrite_rule: "Proof.context -> thm list -> thm -> thm"} \\ + @{define_ML rewrite_goals_rule: "Proof.context -> thm list -> thm -> thm"} \\ + @{define_ML rewrite_goal_tac: "Proof.context -> thm list -> int -> tactic"} \\ + @{define_ML rewrite_goals_tac: "Proof.context -> thm list -> tactic"} \\ + @{define_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\ \end{mldecls} \<^descr> \<^ML>\rewrite_rule\~\ctxt rules thm\ rewrites the whole theorem by the diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Integration.thy --- a/src/Doc/Implementation/Integration.thy Sat May 22 13:35:25 2021 +0200 +++ b/src/Doc/Implementation/Integration.thy Sat May 22 21:52:13 2021 +0200 @@ -37,11 +37,11 @@ text %mlref \ \begin{mldecls} - @{index_ML_type Toplevel.state} \\ - @{index_ML_exception Toplevel.UNDEF} \\ - @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\ - @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\ - @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\ + @{define_ML_type Toplevel.state} \\ + @{define_ML_exception Toplevel.UNDEF} \\ + @{define_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\ + @{define_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\ + @{define_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\Toplevel.state\ represents Isar toplevel states, which are @@ -95,17 +95,17 @@ text %mlref \ \begin{mldecls} - @{index_ML Toplevel.keep: "(Toplevel.state -> unit) -> + @{define_ML Toplevel.keep: "(Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition"} \\ - @{index_ML Toplevel.theory: "(theory -> theory) -> + @{define_ML Toplevel.theory: "(theory -> theory) -> Toplevel.transition -> Toplevel.transition"} \\ - @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) -> + @{define_ML Toplevel.theory_to_proof: "(theory -> Proof.state) -> Toplevel.transition -> Toplevel.transition"} \\ - @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) -> + @{define_ML Toplevel.proof: "(Proof.state -> Proof.state) -> Toplevel.transition -> Toplevel.transition"} \\ - @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) -> + @{define_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) -> Toplevel.transition -> Toplevel.transition"} \\ - @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) -> + @{define_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) -> Toplevel.transition -> Toplevel.transition"} \\ \end{mldecls} @@ -150,10 +150,10 @@ text %mlref \ \begin{mldecls} - @{index_ML use_thy: "string -> unit"} \\ - @{index_ML Thy_Info.get_theory: "string -> theory"} \\ - @{index_ML Thy_Info.remove_thy: "string -> unit"} \\ - @{index_ML Thy_Info.register_thy: "theory -> unit"} \\ + @{define_ML use_thy: "string -> unit"} \\ + @{define_ML Thy_Info.get_theory: "string -> theory"} \\ + @{define_ML Thy_Info.remove_thy: "string -> unit"} \\ + @{define_ML Thy_Info.register_thy: "theory -> unit"} \\ \end{mldecls} \<^descr> \<^ML>\use_thy\~\A\ ensures that theory \A\ is fully up-to-date wrt.\ the diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Isar.thy --- a/src/Doc/Implementation/Isar.thy Sat May 22 13:35:25 2021 +0200 +++ b/src/Doc/Implementation/Isar.thy Sat May 22 21:52:13 2021 +0200 @@ -60,16 +60,16 @@ text %mlref \ \begin{mldecls} - @{index_ML_type Proof.state} \\ - @{index_ML Proof.assert_forward: "Proof.state -> Proof.state"} \\ - @{index_ML Proof.assert_chain: "Proof.state -> Proof.state"} \\ - @{index_ML Proof.assert_backward: "Proof.state -> Proof.state"} \\ - @{index_ML Proof.simple_goal: "Proof.state -> {context: Proof.context, goal: thm}"} \\ - @{index_ML Proof.goal: "Proof.state -> + @{define_ML_type Proof.state} \\ + @{define_ML Proof.assert_forward: "Proof.state -> Proof.state"} \\ + @{define_ML Proof.assert_chain: "Proof.state -> Proof.state"} \\ + @{define_ML Proof.assert_backward: "Proof.state -> Proof.state"} \\ + @{define_ML Proof.simple_goal: "Proof.state -> {context: Proof.context, goal: thm}"} \\ + @{define_ML Proof.goal: "Proof.state -> {context: Proof.context, facts: thm list, goal: thm}"} \\ - @{index_ML Proof.raw_goal: "Proof.state -> + @{define_ML Proof.raw_goal: "Proof.state -> {context: Proof.context, facts: thm list, goal: thm}"} \\ - @{index_ML Proof.theorem: "Method.text option -> + @{define_ML Proof.theorem: "Method.text option -> (thm list list -> Proof.context -> Proof.context) -> (term * term list) list list -> Proof.context -> Proof.state"} \\ \end{mldecls} @@ -272,13 +272,13 @@ text %mlref \ \begin{mldecls} - @{index_ML_type Proof.method} \\ - @{index_ML CONTEXT_METHOD: "(thm list -> context_tactic) -> Proof.method"} \\ - @{index_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\ - @{index_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\ - @{index_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\ - @{index_ML Method.insert_tac: "Proof.context -> thm list -> int -> tactic"} \\ - @{index_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser -> + @{define_ML_type Proof.method} \\ + @{define_ML CONTEXT_METHOD: "(thm list -> context_tactic) -> Proof.method"} \\ + @{define_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\ + @{define_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\ + @{define_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\ + @{define_ML Method.insert_tac: "Proof.context -> thm list -> int -> tactic"} \\ + @{define_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser -> string -> theory -> theory"} \\ \end{mldecls} @@ -286,7 +286,7 @@ \<^descr> \<^ML>\CONTEXT_METHOD\~\(fn facts => context_tactic)\ wraps \context_tactic\ depending on goal facts as a general proof method that may change the proof - context dynamically. A typical operation is \<^ML>\Proof_Context.update_cases\, which is wrapped up as combinator @{index_ML + context dynamically. A typical operation is \<^ML>\Proof_Context.update_cases\, which is wrapped up as combinator @{define_ML CONTEXT_CASES} for convenience. \<^descr> \<^ML>\METHOD\~\(fn facts => tactic)\ wraps \tactic\ depending on goal facts @@ -495,12 +495,12 @@ text %mlref \ \begin{mldecls} - @{index_ML_type attribute} \\ - @{index_ML Thm.rule_attribute: "thm list -> + @{define_ML_type attribute} \\ + @{define_ML Thm.rule_attribute: "thm list -> (Context.generic -> thm -> thm) -> attribute"} \\ - @{index_ML Thm.declaration_attribute: " + @{define_ML Thm.declaration_attribute: " (thm -> Context.generic -> Context.generic) -> attribute"} \\ - @{index_ML Attrib.setup: "binding -> attribute context_parser -> + @{define_ML Attrib.setup: "binding -> attribute context_parser -> string -> theory -> theory"} \\ \end{mldecls} diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Local_Theory.thy --- a/src/Doc/Implementation/Local_Theory.thy Sat May 22 13:35:25 2021 +0200 +++ b/src/Doc/Implementation/Local_Theory.thy Sat May 22 21:52:13 2021 +0200 @@ -90,11 +90,11 @@ text %mlref \ \begin{mldecls} - @{index_ML_type local_theory = Proof.context} \\ - @{index_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex] - @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> + @{define_ML_type local_theory = Proof.context} \\ + @{define_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex] + @{define_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory"} \\ - @{index_ML Local_Theory.note: "Attrib.binding * thm list -> + @{define_ML Local_Theory.note: "Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory"} \\ \end{mldecls} diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Sat May 22 13:35:25 2021 +0200 +++ b/src/Doc/Implementation/Logic.thy Sat May 22 21:52:13 2021 +0200 @@ -102,22 +102,22 @@ text %mlref \ \begin{mldecls} - @{index_ML_type class = string} \\ - @{index_ML_type sort = "class list"} \\ - @{index_ML_type arity = "string * sort list * sort"} \\ - @{index_ML_type typ} \\ - @{index_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\ - @{index_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\ + @{define_ML_type class = string} \\ + @{define_ML_type sort = "class list"} \\ + @{define_ML_type arity = "string * sort list * sort"} \\ + @{define_ML_type typ} \\ + @{define_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\ + @{define_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\ \end{mldecls} \begin{mldecls} - @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\ - @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\ - @{index_ML Sign.add_type: "Proof.context -> binding * int * mixfix -> theory -> theory"} \\ - @{index_ML Sign.add_type_abbrev: "Proof.context -> + @{define_ML Sign.subsort: "theory -> sort * sort -> bool"} \\ + @{define_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\ + @{define_ML Sign.add_type: "Proof.context -> binding * int * mixfix -> theory -> theory"} \\ + @{define_ML Sign.add_type_abbrev: "Proof.context -> binding * string list * typ -> theory -> theory"} \\ - @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\ - @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\ - @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\ + @{define_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\ + @{define_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\ + @{define_ML Sign.primitive_arity: "arity -> theory -> theory"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\class\ represents type classes. @@ -313,30 +313,30 @@ text %mlref \ \begin{mldecls} - @{index_ML_type term} \\ - @{index_ML_infix "aconv": "term * term -> bool"} \\ - @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\ - @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\ - @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\ - @{index_ML Term.fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\ + @{define_ML_type term} \\ + @{define_ML_infix "aconv": "term * term -> bool"} \\ + @{define_ML Term.map_types: "(typ -> typ) -> term -> term"} \\ + @{define_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\ + @{define_ML Term.map_aterms: "(term -> term) -> term -> term"} \\ + @{define_ML Term.fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\ \end{mldecls} \begin{mldecls} - @{index_ML fastype_of: "term -> typ"} \\ - @{index_ML lambda: "term -> term -> term"} \\ - @{index_ML betapply: "term * term -> term"} \\ - @{index_ML incr_boundvars: "int -> term -> term"} \\ - @{index_ML Sign.declare_const: "Proof.context -> + @{define_ML fastype_of: "term -> typ"} \\ + @{define_ML lambda: "term -> term -> term"} \\ + @{define_ML betapply: "term * term -> term"} \\ + @{define_ML incr_boundvars: "int -> term -> term"} \\ + @{define_ML Sign.declare_const: "Proof.context -> (binding * typ) * mixfix -> theory -> term * theory"} \\ - @{index_ML Sign.add_abbrev: "string -> binding * term -> + @{define_ML Sign.add_abbrev: "string -> binding * term -> theory -> (term * term) * theory"} \\ - @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\ - @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\ + @{define_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\ + @{define_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\term\ represents de-Bruijn terms, with comments in abstractions, and explicitly named free variables and constants; this is a - datatype with constructors @{index_ML Bound}, @{index_ML Free}, @{index_ML - Var}, @{index_ML Const}, @{index_ML Abs}, @{index_ML_infix "$"}. + datatype with constructors @{define_ML Bound}, @{define_ML Free}, @{define_ML + Var}, @{define_ML Const}, @{define_ML Abs}, @{define_ML_infix "$"}. \<^descr> \t\~\<^ML_text>\aconv\~\u\ checks \\\-equivalence of two terms. This is the basic equality relation on type \<^ML_type>\term\; raw datatype equality @@ -564,41 +564,41 @@ text %mlref \ \begin{mldecls} - @{index_ML Logic.all: "term -> term -> term"} \\ - @{index_ML Logic.mk_implies: "term * term -> term"} \\ + @{define_ML Logic.all: "term -> term -> term"} \\ + @{define_ML Logic.mk_implies: "term * term -> term"} \\ \end{mldecls} \begin{mldecls} - @{index_ML_type ctyp} \\ - @{index_ML_type cterm} \\ - @{index_ML Thm.ctyp_of: "Proof.context -> typ -> ctyp"} \\ - @{index_ML Thm.cterm_of: "Proof.context -> term -> cterm"} \\ - @{index_ML Thm.apply: "cterm -> cterm -> cterm"} \\ - @{index_ML Thm.lambda: "cterm -> cterm -> cterm"} \\ - @{index_ML Thm.all: "Proof.context -> cterm -> cterm -> cterm"} \\ - @{index_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\ + @{define_ML_type ctyp} \\ + @{define_ML_type cterm} \\ + @{define_ML Thm.ctyp_of: "Proof.context -> typ -> ctyp"} \\ + @{define_ML Thm.cterm_of: "Proof.context -> term -> cterm"} \\ + @{define_ML Thm.apply: "cterm -> cterm -> cterm"} \\ + @{define_ML Thm.lambda: "cterm -> cterm -> cterm"} \\ + @{define_ML Thm.all: "Proof.context -> cterm -> cterm -> cterm"} \\ + @{define_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\ \end{mldecls} \begin{mldecls} - @{index_ML_type thm} \\ - @{index_ML Thm.transfer: "theory -> thm -> thm"} \\ - @{index_ML Thm.assume: "cterm -> thm"} \\ - @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\ - @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\ - @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\ - @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\ - @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\ - @{index_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list + @{define_ML_type thm} \\ + @{define_ML Thm.transfer: "theory -> thm -> thm"} \\ + @{define_ML Thm.assume: "cterm -> thm"} \\ + @{define_ML Thm.forall_intr: "cterm -> thm -> thm"} \\ + @{define_ML Thm.forall_elim: "cterm -> thm -> thm"} \\ + @{define_ML Thm.implies_intr: "cterm -> thm -> thm"} \\ + @{define_ML Thm.implies_elim: "thm -> thm -> thm"} \\ + @{define_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\ + @{define_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm"} \\ - @{index_ML Thm.add_axiom: "Proof.context -> + @{define_ML Thm.add_axiom: "Proof.context -> binding * term -> theory -> (string * thm) * theory"} \\ - @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory -> + @{define_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory"} \\ - @{index_ML Thm.add_def: "Defs.context -> bool -> bool -> + @{define_ML Thm.add_def: "Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory"} \\ \end{mldecls} \begin{mldecls} - @{index_ML Theory.add_deps: "Defs.context -> string -> + @{define_ML Theory.add_deps: "Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory"} \\ - @{index_ML Thm_Deps.all_oracles: "thm list -> Proofterm.oracle list"} \\ + @{define_ML Thm_Deps.all_oracles: "thm list -> Proofterm.oracle list"} \\ \end{mldecls} \<^descr> \<^ML>\Logic.all\~\a B\ produces a Pure quantification \\a. B\, where @@ -796,12 +796,12 @@ text %mlref \ \begin{mldecls} - @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\ - @{index_ML Conjunction.elim: "thm -> thm * thm"} \\ - @{index_ML Drule.mk_term: "cterm -> thm"} \\ - @{index_ML Drule.dest_term: "thm -> cterm"} \\ - @{index_ML Logic.mk_type: "typ -> term"} \\ - @{index_ML Logic.dest_type: "term -> typ"} \\ + @{define_ML Conjunction.intr: "thm -> thm -> thm"} \\ + @{define_ML Conjunction.elim: "thm -> thm * thm"} \\ + @{define_ML Drule.mk_term: "cterm -> thm"} \\ + @{define_ML Drule.dest_term: "thm -> cterm"} \\ + @{define_ML Logic.mk_type: "typ -> term"} \\ + @{define_ML Logic.dest_type: "term -> typ"} \\ \end{mldecls} \<^descr> \<^ML>\Conjunction.intr\ derives \A &&& B\ from \A\ and \B\. @@ -846,8 +846,8 @@ text %mlref \ \begin{mldecls} - @{index_ML Thm.extra_shyps: "thm -> sort list"} \\ - @{index_ML Thm.strip_shyps: "thm -> thm"} \\ + @{define_ML Thm.extra_shyps: "thm -> sort list"} \\ + @{define_ML Thm.strip_shyps: "thm -> thm"} \\ \end{mldecls} \<^descr> \<^ML>\Thm.extra_shyps\~\thm\ determines the extraneous sort hypotheses of @@ -951,7 +951,7 @@ text %mlref \ \begin{mldecls} - @{index_ML Simplifier.norm_hhf: "Proof.context -> thm -> thm"} \\ + @{define_ML Simplifier.norm_hhf: "Proof.context -> thm -> thm"} \\ \end{mldecls} \<^descr> \<^ML>\Simplifier.norm_hhf\~\ctxt thm\ normalizes the given theorem @@ -1022,14 +1022,14 @@ text %mlref \ \begin{mldecls} - @{index_ML_infix "RSN": "thm * (int * thm) -> thm"} \\ - @{index_ML_infix "RS": "thm * thm -> thm"} \\ + @{define_ML_infix "RSN": "thm * (int * thm) -> thm"} \\ + @{define_ML_infix "RS": "thm * thm -> thm"} \\ - @{index_ML_infix "RLN": "thm list * (int * thm list) -> thm list"} \\ - @{index_ML_infix "RL": "thm list * thm list -> thm list"} \\ + @{define_ML_infix "RLN": "thm list * (int * thm list) -> thm list"} \\ + @{define_ML_infix "RL": "thm list * thm list -> thm list"} \\ - @{index_ML_infix "MRS": "thm list * thm -> thm"} \\ - @{index_ML_infix "OF": "thm * thm list -> thm"} \\ + @{define_ML_infix "MRS": "thm list * thm -> thm"} \\ + @{define_ML_infix "OF": "thm * thm list -> thm"} \\ \end{mldecls} \<^descr> \rule\<^sub>1 RSN (i, rule\<^sub>2)\ resolves the conclusion of \rule\<^sub>1\ with the @@ -1184,22 +1184,22 @@ text %mlref \ \begin{mldecls} - @{index_ML_type proof} \\ - @{index_ML_type proof_body} \\ - @{index_ML Proofterm.proofs: "int Unsynchronized.ref"} \\ - @{index_ML Proofterm.reconstruct_proof: + @{define_ML_type proof} \\ + @{define_ML_type proof_body} \\ + @{define_ML Proofterm.proofs: "int Unsynchronized.ref"} \\ + @{define_ML Proofterm.reconstruct_proof: "theory -> term -> proof -> proof"} \\ - @{index_ML Proofterm.expand_proof: "theory -> + @{define_ML Proofterm.expand_proof: "theory -> (Proofterm.thm_header -> string option) -> proof -> proof"} \\ - @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\ - @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\ - @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\ + @{define_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\ + @{define_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\ + @{define_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\proof\ represents proof terms; this is a datatype with - constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_infix "%"}, - @{index_ML_infix "%%"}, @{index_ML PBound}, @{index_ML MinProof}, @{index_ML - Hyp}, @{index_ML PAxm}, @{index_ML Oracle}, @{index_ML PThm} as explained + constructors @{define_ML Abst}, @{define_ML AbsP}, @{define_ML_infix "%"}, + @{define_ML_infix "%%"}, @{define_ML PBound}, @{define_ML MinProof}, @{define_ML + Hyp}, @{define_ML PAxm}, @{define_ML Oracle}, @{define_ML PThm} as explained above. %FIXME PClass (!?) \<^descr> Type \<^ML_type>\proof_body\ represents the nested proof information of a diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Sat May 22 13:35:25 2021 +0200 +++ b/src/Doc/Implementation/ML.thy Sat May 22 21:52:13 2021 +0200 @@ -611,10 +611,10 @@ text %mlref \ \begin{mldecls} - @{index_ML Context.the_generic_context: "unit -> Context.generic"} \\ - @{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\ - @{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\ - @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\ + @{define_ML Context.the_generic_context: "unit -> Context.generic"} \\ + @{define_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\ + @{define_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\ + @{define_ML ML_Thms.bind_thm: "string * thm -> unit"} \\ \end{mldecls} \<^descr> \<^ML>\Context.the_generic_context ()\ refers to the theory context of @@ -818,10 +818,10 @@ text %mlref \ \begin{mldecls} - @{index_ML_infix "|>" : "'a * ('a -> 'b) -> 'b"} \\ - @{index_ML_infix "|->" : "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\ - @{index_ML_infix "#>" : "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\ - @{index_ML_infix "#->" : "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\ + @{define_ML_infix "|>" : "'a * ('a -> 'b) -> 'b"} \\ + @{define_ML_infix "|->" : "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\ + @{define_ML_infix "#>" : "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\ + @{define_ML_infix "#->" : "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\ \end{mldecls} \ @@ -853,9 +853,9 @@ text %mlref \ \begin{mldecls} - @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\ - @{index_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\ - @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\ + @{define_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\ + @{define_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\ + @{define_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\ \end{mldecls} \<^descr> \<^ML>\fold\~\f\ lifts the parametrized update function \f\ to a list of @@ -969,10 +969,10 @@ text %mlref \ \begin{mldecls} - @{index_ML writeln: "string -> unit"} \\ - @{index_ML tracing: "string -> unit"} \\ - @{index_ML warning: "string -> unit"} \\ - @{index_ML error: "string -> 'a"} % FIXME Output.error_message (!?) \\ + @{define_ML writeln: "string -> unit"} \\ + @{define_ML tracing: "string -> unit"} \\ + @{define_ML warning: "string -> unit"} \\ + @{define_ML error: "string -> 'a"} % FIXME Output.error_message (!?) \\ \end{mldecls} \<^descr> \<^ML>\writeln\~\text\ outputs \text\ as regular message. This is the @@ -1140,13 +1140,13 @@ text %mlref \ \begin{mldecls} - @{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\ - @{index_ML can: "('a -> 'b) -> 'a -> bool"} \\ - @{index_ML_exception ERROR of string} \\ - @{index_ML_exception Fail of string} \\ - @{index_ML Exn.is_interrupt: "exn -> bool"} \\ - @{index_ML Exn.reraise: "exn -> 'a"} \\ - @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\ + @{define_ML try: "('a -> 'b) -> 'a -> 'b option"} \\ + @{define_ML can: "('a -> 'b) -> 'a -> bool"} \\ + @{define_ML_exception ERROR of string} \\ + @{define_ML_exception Fail of string} \\ + @{define_ML Exn.is_interrupt: "exn -> bool"} \\ + @{define_ML Exn.reraise: "exn -> 'a"} \\ + @{define_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\ \end{mldecls} \<^rail>\ @@ -1284,16 +1284,16 @@ text %mlref \ \begin{mldecls} - @{index_ML_type Symbol.symbol = string} \\ - @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\ - @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\ - @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\ - @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\ - @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\ + @{define_ML_type Symbol.symbol = string} \\ + @{define_ML Symbol.explode: "string -> Symbol.symbol list"} \\ + @{define_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\ + @{define_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\ + @{define_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\ + @{define_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\ \end{mldecls} \begin{mldecls} - @{index_ML_type "Symbol.sym"} \\ - @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\ + @{define_ML_type "Symbol.sym"} \\ + @{define_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\Symbol.symbol\ represents individual Isabelle symbols. @@ -1347,7 +1347,7 @@ text %mlref \ \begin{mldecls} - @{index_ML_type char} \\ + @{define_ML_type char} \\ \end{mldecls} \<^descr> Type \<^ML_type>\char\ is \<^emph>\not\ used. The smallest textual unit in Isabelle @@ -1359,7 +1359,7 @@ text %mlref \ \begin{mldecls} - @{index_ML_type string} \\ + @{define_ML_type string} \\ \end{mldecls} \<^descr> Type \<^ML_type>\string\ represents immutable vectors of 8-bit characters. @@ -1407,7 +1407,7 @@ text %mlref \ \begin{mldecls} - @{index_ML_type int} \\ + @{define_ML_type int} \\ \end{mldecls} \<^descr> Type \<^ML_type>\int\ represents regular mathematical integers, which are @@ -1425,7 +1425,7 @@ text %mlref \ \begin{mldecls} - @{index_ML_type Rat.rat} \\ + @{define_ML_type Rat.rat} \\ \end{mldecls} \<^descr> Type \<^ML_type>\Rat.rat\ represents rational numbers, based on the @@ -1444,8 +1444,8 @@ text %mlref \ \begin{mldecls} - @{index_ML_type Time.time} \\ - @{index_ML seconds: "real -> Time.time"} \\ + @{define_ML_type Time.time} \\ + @{define_ML seconds: "real -> Time.time"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\Time.time\ represents time abstractly according to the @@ -1463,13 +1463,13 @@ text %mlref \ \begin{mldecls} - @{index_ML Option.map: "('a -> 'b) -> 'a option -> 'b option"} \\ - @{index_ML is_some: "'a option -> bool"} \\ - @{index_ML is_none: "'a option -> bool"} \\ - @{index_ML the: "'a option -> 'a"} \\ - @{index_ML these: "'a list option -> 'a list"} \\ - @{index_ML the_list: "'a option -> 'a list"} \\ - @{index_ML the_default: "'a -> 'a option -> 'a"} \\ + @{define_ML Option.map: "('a -> 'b) -> 'a option -> 'b option"} \\ + @{define_ML is_some: "'a option -> bool"} \\ + @{define_ML is_none: "'a option -> bool"} \\ + @{define_ML the: "'a option -> 'a"} \\ + @{define_ML these: "'a list option -> 'a list"} \\ + @{define_ML the_list: "'a option -> 'a list"} \\ + @{define_ML the_default: "'a -> 'a option -> 'a"} \\ \end{mldecls} \ @@ -1490,11 +1490,11 @@ text %mlref \ \begin{mldecls} - @{index_ML cons: "'a -> 'a list -> 'a list"} \\ - @{index_ML member: "('b * 'a -> bool) -> 'a list -> 'b -> bool"} \\ - @{index_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\ - @{index_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\ - @{index_ML update: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\ + @{define_ML cons: "'a -> 'a list -> 'a list"} \\ + @{define_ML member: "('b * 'a -> bool) -> 'a list -> 'b -> bool"} \\ + @{define_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\ + @{define_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\ + @{define_ML update: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\ \end{mldecls} \<^descr> \<^ML>\cons\~\x xs\ evaluates to \x :: xs\. @@ -1563,9 +1563,9 @@ text \ \begin{mldecls} - @{index_ML AList.lookup: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option"} \\ - @{index_ML AList.defined: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool"} \\ - @{index_ML AList.update: "('a * 'a -> bool) -> 'a * 'b -> ('a * 'b) list -> ('a * 'b) list"} \\ + @{define_ML AList.lookup: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option"} \\ + @{define_ML AList.defined: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool"} \\ + @{define_ML AList.update: "('a * 'a -> bool) -> 'a * 'b -> ('a * 'b) list -> ('a * 'b) list"} \\ \end{mldecls} \<^descr> \<^ML>\AList.lookup\, \<^ML>\AList.defined\, \<^ML>\AList.update\ implement the @@ -1593,10 +1593,10 @@ text %mlref \ \begin{mldecls} - @{index_ML_type "'a Unsynchronized.ref"} \\ - @{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\ - @{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\ - @{index_ML_infix ":=" : "'a Unsynchronized.ref * 'a -> unit"} \\ + @{define_ML_type "'a Unsynchronized.ref"} \\ + @{define_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\ + @{define_ML "!": "'a Unsynchronized.ref -> 'a"} \\ + @{define_ML_infix ":=" : "'a Unsynchronized.ref * 'a -> unit"} \\ \end{mldecls} \ @@ -1748,8 +1748,8 @@ text %mlref \ \begin{mldecls} - @{index_ML File.tmp_path: "Path.T -> Path.T"} \\ - @{index_ML serial_string: "unit -> string"} \\ + @{define_ML File.tmp_path: "Path.T -> Path.T"} \\ + @{define_ML serial_string: "unit -> string"} \\ \end{mldecls} \<^descr> \<^ML>\File.tmp_path\~\path\ relocates the base component of \path\ into the @@ -1790,9 +1790,9 @@ text %mlref \ \begin{mldecls} - @{index_ML_type "'a Synchronized.var"} \\ - @{index_ML Synchronized.var: "string -> 'a -> 'a Synchronized.var"} \\ - @{index_ML Synchronized.guarded_access: "'a Synchronized.var -> + @{define_ML_type "'a Synchronized.var"} \\ + @{define_ML Synchronized.var: "string -> 'a -> 'a Synchronized.var"} \\ + @{define_ML Synchronized.guarded_access: "'a Synchronized.var -> ('a -> ('b * 'a) option) -> 'b"} \\ \end{mldecls} @@ -1890,12 +1890,12 @@ text %mlref \ \begin{mldecls} - @{index_ML_type "'a Exn.result"} \\ - @{index_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\ - @{index_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\ - @{index_ML Exn.release: "'a Exn.result -> 'a"} \\ - @{index_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\ - @{index_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\ + @{define_ML_type "'a Exn.result"} \\ + @{define_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\ + @{define_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\ + @{define_ML Exn.release: "'a Exn.result -> 'a"} \\ + @{define_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\ + @{define_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\'a Exn.result\ represents the disjoint sum of ML results @@ -1945,8 +1945,8 @@ text %mlref \ \begin{mldecls} - @{index_ML Par_List.map: "('a -> 'b) -> 'a list -> 'b list"} \\ - @{index_ML Par_List.get_some: "('a -> 'b option) -> 'a list -> 'b option"} \\ + @{define_ML Par_List.map: "('a -> 'b) -> 'a list -> 'b list"} \\ + @{define_ML Par_List.get_some: "('a -> 'b option) -> 'a list -> 'b option"} \\ \end{mldecls} \<^descr> \<^ML>\Par_List.map\~\f [x\<^sub>1, \, x\<^sub>n]\ is like \<^ML>\map\~\f [x\<^sub>1, \, @@ -2009,10 +2009,10 @@ text %mlref \ \begin{mldecls} - @{index_ML_type "'a lazy"} \\ - @{index_ML Lazy.lazy: "(unit -> 'a) -> 'a lazy"} \\ - @{index_ML Lazy.value: "'a -> 'a lazy"} \\ - @{index_ML Lazy.force: "'a lazy -> 'a"} \\ + @{define_ML_type "'a lazy"} \\ + @{define_ML Lazy.lazy: "(unit -> 'a) -> 'a lazy"} \\ + @{define_ML Lazy.value: "'a -> 'a lazy"} \\ + @{define_ML Lazy.force: "'a lazy -> 'a"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\'a lazy\ represents lazy values over type \<^verbatim>\'a\. @@ -2090,17 +2090,17 @@ text %mlref \ \begin{mldecls} - @{index_ML_type "'a future"} \\ - @{index_ML Future.fork: "(unit -> 'a) -> 'a future"} \\ - @{index_ML Future.forks: "Future.params -> (unit -> 'a) list -> 'a future list"} \\ - @{index_ML Future.join: "'a future -> 'a"} \\ - @{index_ML Future.joins: "'a future list -> 'a list"} \\ - @{index_ML Future.value: "'a -> 'a future"} \\ - @{index_ML Future.map: "('a -> 'b) -> 'a future -> 'b future"} \\ - @{index_ML Future.cancel: "'a future -> unit"} \\ - @{index_ML Future.cancel_group: "Future.group -> unit"} \\[0.5ex] - @{index_ML Future.promise: "(unit -> unit) -> 'a future"} \\ - @{index_ML Future.fulfill: "'a future -> 'a -> unit"} \\ + @{define_ML_type "'a future"} \\ + @{define_ML Future.fork: "(unit -> 'a) -> 'a future"} \\ + @{define_ML Future.forks: "Future.params -> (unit -> 'a) list -> 'a future list"} \\ + @{define_ML Future.join: "'a future -> 'a"} \\ + @{define_ML Future.joins: "'a future list -> 'a list"} \\ + @{define_ML Future.value: "'a -> 'a future"} \\ + @{define_ML Future.map: "('a -> 'b) -> 'a future -> 'b future"} \\ + @{define_ML Future.cancel: "'a future -> unit"} \\ + @{define_ML Future.cancel_group: "Future.group -> unit"} \\[0.5ex] + @{define_ML Future.promise: "(unit -> unit) -> 'a future"} \\ + @{define_ML Future.fulfill: "'a future -> 'a -> unit"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\'a future\ represents future values over type \<^verbatim>\'a\. diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Prelim.thy --- a/src/Doc/Implementation/Prelim.thy Sat May 22 13:35:25 2021 +0200 +++ b/src/Doc/Implementation/Prelim.thy Sat May 22 21:52:13 2021 +0200 @@ -108,12 +108,12 @@ text %mlref \ \begin{mldecls} - @{index_ML_type theory} \\ - @{index_ML Context.eq_thy: "theory * theory -> bool"} \\ - @{index_ML Context.subthy: "theory * theory -> bool"} \\ - @{index_ML Theory.begin_theory: "string * Position.T -> theory list -> theory"} \\ - @{index_ML Theory.parents_of: "theory -> theory list"} \\ - @{index_ML Theory.ancestors_of: "theory -> theory list"} \\ + @{define_ML_type theory} \\ + @{define_ML Context.eq_thy: "theory * theory -> bool"} \\ + @{define_ML Context.subthy: "theory * theory -> bool"} \\ + @{define_ML Theory.begin_theory: "string * Position.T -> theory list -> theory"} \\ + @{define_ML Theory.parents_of: "theory -> theory list"} \\ + @{define_ML Theory.ancestors_of: "theory -> theory list"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\theory\ represents theory contexts. @@ -187,10 +187,10 @@ text %mlref \ \begin{mldecls} - @{index_ML_type Proof.context} \\ - @{index_ML Proof_Context.init_global: "theory -> Proof.context"} \\ - @{index_ML Proof_Context.theory_of: "Proof.context -> theory"} \\ - @{index_ML Proof_Context.transfer: "theory -> Proof.context -> Proof.context"} \\ + @{define_ML_type Proof.context} \\ + @{define_ML Proof_Context.init_global: "theory -> Proof.context"} \\ + @{define_ML Proof_Context.theory_of: "Proof.context -> theory"} \\ + @{define_ML Proof_Context.transfer: "theory -> Proof.context -> Proof.context"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\Proof.context\ represents proof contexts. @@ -236,9 +236,9 @@ text %mlref \ \begin{mldecls} - @{index_ML_type Context.generic} \\ - @{index_ML Context.theory_of: "Context.generic -> theory"} \\ - @{index_ML Context.proof_of: "Context.generic -> Proof.context"} \\ + @{define_ML_type Context.generic} \\ + @{define_ML Context.theory_of: "Context.generic -> theory"} \\ + @{define_ML Context.proof_of: "Context.generic -> Proof.context"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\Context.generic\ is the direct sum of \<^ML_type>\theory\ @@ -339,9 +339,9 @@ text %mlref \ \begin{mldecls} - @{index_ML_functor Theory_Data} \\ - @{index_ML_functor Proof_Data} \\ - @{index_ML_functor Generic_Data} \\ + @{define_ML_functor Theory_Data} \\ + @{define_ML_functor Proof_Data} \\ + @{define_ML_functor Generic_Data} \\ \end{mldecls} \<^descr> \<^ML_functor>\Theory_Data\\(spec)\ declares data for type \<^ML_type>\theory\ @@ -482,15 +482,15 @@ text %mlref \ \begin{mldecls} - @{index_ML Config.get: "Proof.context -> 'a Config.T -> 'a"} \\ - @{index_ML Config.map: "'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context"} \\ - @{index_ML Attrib.setup_config_bool: "binding -> (Context.generic -> bool) -> + @{define_ML Config.get: "Proof.context -> 'a Config.T -> 'a"} \\ + @{define_ML Config.map: "'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context"} \\ + @{define_ML Attrib.setup_config_bool: "binding -> (Context.generic -> bool) -> bool Config.T"} \\ - @{index_ML Attrib.setup_config_int: "binding -> (Context.generic -> int) -> + @{define_ML Attrib.setup_config_int: "binding -> (Context.generic -> int) -> int Config.T"} \\ - @{index_ML Attrib.setup_config_real: "binding -> (Context.generic -> real) -> + @{define_ML Attrib.setup_config_real: "binding -> (Context.generic -> real) -> real Config.T"} \\ - @{index_ML Attrib.setup_config_string: "binding -> (Context.generic -> string) -> + @{define_ML Attrib.setup_config_string: "binding -> (Context.generic -> string) -> string Config.T"} \\ \end{mldecls} @@ -613,18 +613,18 @@ text %mlref \ \begin{mldecls} - @{index_ML Name.internal: "string -> string"} \\ - @{index_ML Name.skolem: "string -> string"} \\ + @{define_ML Name.internal: "string -> string"} \\ + @{define_ML Name.skolem: "string -> string"} \\ \end{mldecls} \begin{mldecls} - @{index_ML_type Name.context} \\ - @{index_ML Name.context: Name.context} \\ - @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\ - @{index_ML Name.invent: "Name.context -> string -> int -> string list"} \\ - @{index_ML Name.variant: "string -> Name.context -> string * Name.context"} \\ + @{define_ML_type Name.context} \\ + @{define_ML Name.context: Name.context} \\ + @{define_ML Name.declare: "string -> Name.context -> Name.context"} \\ + @{define_ML Name.invent: "Name.context -> string -> int -> string list"} \\ + @{define_ML Name.variant: "string -> Name.context -> string * Name.context"} \\ \end{mldecls} \begin{mldecls} - @{index_ML Variable.names_of: "Proof.context -> Name.context"} \\ + @{define_ML Variable.names_of: "Proof.context -> Name.context"} \\ \end{mldecls} \<^descr> \<^ML>\Name.internal\~\name\ produces an internal name by adding one @@ -720,7 +720,7 @@ text %mlref \ \begin{mldecls} - @{index_ML_type indexname = "string * int"} \\ + @{define_ML_type indexname = "string * int"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\indexname\ represents indexed names. This is an @@ -755,11 +755,11 @@ text %mlref \ \begin{mldecls} - @{index_ML Long_Name.base_name: "string -> string"} \\ - @{index_ML Long_Name.qualifier: "string -> string"} \\ - @{index_ML Long_Name.append: "string -> string -> string"} \\ - @{index_ML Long_Name.implode: "string list -> string"} \\ - @{index_ML Long_Name.explode: "string -> string list"} \\ + @{define_ML Long_Name.base_name: "string -> string"} \\ + @{define_ML Long_Name.qualifier: "string -> string"} \\ + @{define_ML Long_Name.append: "string -> string -> string"} \\ + @{define_ML Long_Name.implode: "string list -> string"} \\ + @{define_ML Long_Name.explode: "string -> string list"} \\ \end{mldecls} \<^descr> \<^ML>\Long_Name.base_name\~\name\ returns the base name of a long name. @@ -832,29 +832,29 @@ text %mlref \ \begin{mldecls} - @{index_ML_type binding} \\ - @{index_ML Binding.empty: binding} \\ - @{index_ML Binding.name: "string -> binding"} \\ - @{index_ML Binding.qualify: "bool -> string -> binding -> binding"} \\ - @{index_ML Binding.prefix: "bool -> string -> binding -> binding"} \\ - @{index_ML Binding.concealed: "binding -> binding"} \\ - @{index_ML Binding.print: "binding -> string"} \\ + @{define_ML_type binding} \\ + @{define_ML Binding.empty: binding} \\ + @{define_ML Binding.name: "string -> binding"} \\ + @{define_ML Binding.qualify: "bool -> string -> binding -> binding"} \\ + @{define_ML Binding.prefix: "bool -> string -> binding -> binding"} \\ + @{define_ML Binding.concealed: "binding -> binding"} \\ + @{define_ML Binding.print: "binding -> string"} \\ \end{mldecls} \begin{mldecls} - @{index_ML_type Name_Space.naming} \\ - @{index_ML Name_Space.global_naming: Name_Space.naming} \\ - @{index_ML Name_Space.add_path: "string -> Name_Space.naming -> Name_Space.naming"} \\ - @{index_ML Name_Space.full_name: "Name_Space.naming -> binding -> string"} \\ + @{define_ML_type Name_Space.naming} \\ + @{define_ML Name_Space.global_naming: Name_Space.naming} \\ + @{define_ML Name_Space.add_path: "string -> Name_Space.naming -> Name_Space.naming"} \\ + @{define_ML Name_Space.full_name: "Name_Space.naming -> binding -> string"} \\ \end{mldecls} \begin{mldecls} - @{index_ML_type Name_Space.T} \\ - @{index_ML Name_Space.empty: "string -> Name_Space.T"} \\ - @{index_ML Name_Space.merge: "Name_Space.T * Name_Space.T -> Name_Space.T"} \\ - @{index_ML Name_Space.declare: "Context.generic -> bool -> + @{define_ML_type Name_Space.T} \\ + @{define_ML Name_Space.empty: "string -> Name_Space.T"} \\ + @{define_ML Name_Space.merge: "Name_Space.T * Name_Space.T -> Name_Space.T"} \\ + @{define_ML Name_Space.declare: "Context.generic -> bool -> binding -> Name_Space.T -> string * Name_Space.T"} \\ - @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\ - @{index_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\ - @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"} + @{define_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\ + @{define_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\ + @{define_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"} \end{mldecls} \<^descr> Type \<^ML_type>\binding\ represents the abstract concept of name bindings. diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Proof.thy --- a/src/Doc/Implementation/Proof.thy Sat May 22 13:35:25 2021 +0200 +++ b/src/Doc/Implementation/Proof.thy Sat May 22 21:52:13 2021 +0200 @@ -92,18 +92,18 @@ text %mlref \ \begin{mldecls} - @{index_ML Variable.add_fixes: " + @{define_ML Variable.add_fixes: " string list -> Proof.context -> string list * Proof.context"} \\ - @{index_ML Variable.variant_fixes: " + @{define_ML Variable.variant_fixes: " string list -> Proof.context -> string list * Proof.context"} \\ - @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\ - @{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\ - @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\ - @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ - @{index_ML Variable.import: "bool -> thm list -> Proof.context -> + @{define_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\ + @{define_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\ + @{define_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\ + @{define_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ + @{define_ML Variable.import: "bool -> thm list -> Proof.context -> ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context"} \\ - @{index_ML Variable.focus: "binding list option -> term -> Proof.context -> + @{define_ML Variable.focus: "binding list option -> term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context"} \\ \end{mldecls} @@ -263,14 +263,14 @@ text %mlref \ \begin{mldecls} - @{index_ML_type Assumption.export} \\ - @{index_ML Assumption.assume: "Proof.context -> cterm -> thm"} \\ - @{index_ML Assumption.add_assms: + @{define_ML_type Assumption.export} \\ + @{define_ML Assumption.assume: "Proof.context -> cterm -> thm"} \\ + @{define_ML Assumption.add_assms: "Assumption.export -> cterm list -> Proof.context -> thm list * Proof.context"} \\ - @{index_ML Assumption.add_assumes: " + @{define_ML Assumption.add_assumes: " cterm list -> Proof.context -> thm list * Proof.context"} \\ - @{index_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\ + @{define_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\Assumption.export\ represents arbitrary export rules, which @@ -359,31 +359,31 @@ text %mlref \ \begin{mldecls} - @{index_ML SUBPROOF: "(Subgoal.focus -> tactic) -> + @{define_ML SUBPROOF: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\ - @{index_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) -> + @{define_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\ - @{index_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus -> tactic) -> + @{define_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\ - @{index_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) -> + @{define_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\ - @{index_ML Subgoal.focus: "Proof.context -> int -> binding list option -> + @{define_ML Subgoal.focus: "Proof.context -> int -> binding list option -> thm -> Subgoal.focus * thm"} \\ - @{index_ML Subgoal.focus_prems: "Proof.context -> int -> binding list option -> + @{define_ML Subgoal.focus_prems: "Proof.context -> int -> binding list option -> thm -> Subgoal.focus * thm"} \\ - @{index_ML Subgoal.focus_params: "Proof.context -> int -> binding list option -> + @{define_ML Subgoal.focus_params: "Proof.context -> int -> binding list option -> thm -> Subgoal.focus * thm"} \\ \end{mldecls} \begin{mldecls} - @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term -> + @{define_ML Goal.prove: "Proof.context -> string list -> term list -> term -> ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\ - @{index_ML Goal.prove_common: "Proof.context -> int option -> + @{define_ML Goal.prove_common: "Proof.context -> int option -> string list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\ \end{mldecls} \begin{mldecls} - @{index_ML Obtain.result: "(Proof.context -> tactic) -> thm list -> + @{define_ML Obtain.result: "(Proof.context -> tactic) -> thm list -> Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\ \end{mldecls} diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Syntax.thy --- a/src/Doc/Implementation/Syntax.thy Sat May 22 13:35:25 2021 +0200 +++ b/src/Doc/Implementation/Syntax.thy Sat May 22 21:52:13 2021 +0200 @@ -69,16 +69,16 @@ text %mlref \ \begin{mldecls} - @{index_ML Syntax.read_typs: "Proof.context -> string list -> typ list"} \\ - @{index_ML Syntax.read_terms: "Proof.context -> string list -> term list"} \\ - @{index_ML Syntax.read_props: "Proof.context -> string list -> term list"} \\[0.5ex] - @{index_ML Syntax.read_typ: "Proof.context -> string -> typ"} \\ - @{index_ML Syntax.read_term: "Proof.context -> string -> term"} \\ - @{index_ML Syntax.read_prop: "Proof.context -> string -> term"} \\[0.5ex] - @{index_ML Syntax.pretty_typ: "Proof.context -> typ -> Pretty.T"} \\ - @{index_ML Syntax.pretty_term: "Proof.context -> term -> Pretty.T"} \\ - @{index_ML Syntax.string_of_typ: "Proof.context -> typ -> string"} \\ - @{index_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\ + @{define_ML Syntax.read_typs: "Proof.context -> string list -> typ list"} \\ + @{define_ML Syntax.read_terms: "Proof.context -> string list -> term list"} \\ + @{define_ML Syntax.read_props: "Proof.context -> string list -> term list"} \\[0.5ex] + @{define_ML Syntax.read_typ: "Proof.context -> string -> typ"} \\ + @{define_ML Syntax.read_term: "Proof.context -> string -> term"} \\ + @{define_ML Syntax.read_prop: "Proof.context -> string -> term"} \\[0.5ex] + @{define_ML Syntax.pretty_typ: "Proof.context -> typ -> Pretty.T"} \\ + @{define_ML Syntax.pretty_term: "Proof.context -> term -> Pretty.T"} \\ + @{define_ML Syntax.string_of_typ: "Proof.context -> typ -> string"} \\ + @{define_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\ \end{mldecls} \<^descr> \<^ML>\Syntax.read_typs\~\ctxt strs\ parses and checks a simultaneous list @@ -158,11 +158,11 @@ text %mlref \ \begin{mldecls} - @{index_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\ - @{index_ML Syntax.parse_term: "Proof.context -> string -> term"} \\ - @{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\[0.5ex] - @{index_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\ - @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\ + @{define_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\ + @{define_ML Syntax.parse_term: "Proof.context -> string -> term"} \\ + @{define_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\[0.5ex] + @{define_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\ + @{define_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\ \end{mldecls} \<^descr> \<^ML>\Syntax.parse_typ\~\ctxt str\ parses a source string as pre-type that @@ -219,11 +219,11 @@ text %mlref \ \begin{mldecls} - @{index_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\ - @{index_ML Syntax.check_terms: "Proof.context -> term list -> term list"} \\ - @{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\[0.5ex] - @{index_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\ - @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\ + @{define_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\ + @{define_ML Syntax.check_terms: "Proof.context -> term list -> term list"} \\ + @{define_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\[0.5ex] + @{define_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\ + @{define_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\ \end{mldecls} \<^descr> \<^ML>\Syntax.check_typs\~\ctxt Ts\ checks a simultaneous list of pre-types diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Implementation/Tactic.thy --- a/src/Doc/Implementation/Tactic.thy Sat May 22 13:35:25 2021 +0200 +++ b/src/Doc/Implementation/Tactic.thy Sat May 22 21:52:13 2021 +0200 @@ -61,10 +61,10 @@ text %mlref \ \begin{mldecls} - @{index_ML Goal.init: "cterm -> thm"} \\ - @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\ - @{index_ML Goal.protect: "int -> thm -> thm"} \\ - @{index_ML Goal.conclude: "thm -> thm"} \\ + @{define_ML Goal.init: "cterm -> thm"} \\ + @{define_ML Goal.finish: "Proof.context -> thm -> thm"} \\ + @{define_ML Goal.protect: "int -> thm -> thm"} \\ + @{define_ML Goal.conclude: "thm -> thm"} \\ \end{mldecls} \<^descr> \<^ML>\Goal.init\~\C\ initializes a tactical goal from the well-formed @@ -156,15 +156,15 @@ text %mlref \ \begin{mldecls} - @{index_ML_type tactic = "thm -> thm Seq.seq"} \\ - @{index_ML no_tac: tactic} \\ - @{index_ML all_tac: tactic} \\ - @{index_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex] - @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex] - @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\ - @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\ - @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\ - @{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\ + @{define_ML_type tactic = "thm -> thm Seq.seq"} \\ + @{define_ML no_tac: tactic} \\ + @{define_ML all_tac: tactic} \\ + @{define_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex] + @{define_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex] + @{define_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\ + @{define_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\ + @{define_ML SELECT_GOAL: "tactic -> int -> tactic"} \\ + @{define_ML PREFER_GOAL: "tactic -> int -> tactic"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\tactic\ represents tactics. The well-formedness conditions @@ -243,17 +243,17 @@ text %mlref \ \begin{mldecls} - @{index_ML resolve_tac: "Proof.context -> thm list -> int -> tactic"} \\ - @{index_ML eresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\ - @{index_ML dresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\ - @{index_ML forward_tac: "Proof.context -> thm list -> int -> tactic"} \\ - @{index_ML biresolve_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\[1ex] - @{index_ML assume_tac: "Proof.context -> int -> tactic"} \\ - @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex] - @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\ - @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\ - @{index_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\ - @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\ + @{define_ML resolve_tac: "Proof.context -> thm list -> int -> tactic"} \\ + @{define_ML eresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\ + @{define_ML dresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\ + @{define_ML forward_tac: "Proof.context -> thm list -> int -> tactic"} \\ + @{define_ML biresolve_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\[1ex] + @{define_ML assume_tac: "Proof.context -> int -> tactic"} \\ + @{define_ML eq_assume_tac: "int -> tactic"} \\[1ex] + @{define_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\ + @{define_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\ + @{define_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\ + @{define_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\ \end{mldecls} \<^descr> \<^ML>\resolve_tac\~\ctxt thms i\ refines the goal state using the given @@ -351,23 +351,23 @@ text %mlref \ \begin{mldecls} - @{index_ML Rule_Insts.res_inst_tac: "Proof.context -> + @{define_ML Rule_Insts.res_inst_tac: "Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic"} \\ - @{index_ML Rule_Insts.eres_inst_tac: "Proof.context -> + @{define_ML Rule_Insts.eres_inst_tac: "Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic"} \\ - @{index_ML Rule_Insts.dres_inst_tac: "Proof.context -> + @{define_ML Rule_Insts.dres_inst_tac: "Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic"} \\ - @{index_ML Rule_Insts.forw_inst_tac: "Proof.context -> + @{define_ML Rule_Insts.forw_inst_tac: "Proof.context -> ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm -> int -> tactic"} \\ - @{index_ML Rule_Insts.subgoal_tac: "Proof.context -> string -> + @{define_ML Rule_Insts.subgoal_tac: "Proof.context -> string -> (binding * string option * mixfix) list -> int -> tactic"} \\ - @{index_ML Rule_Insts.thin_tac: "Proof.context -> string -> + @{define_ML Rule_Insts.thin_tac: "Proof.context -> string -> (binding * string option * mixfix) list -> int -> tactic"} \\ - @{index_ML rename_tac: "string list -> int -> tactic"} \\ + @{define_ML rename_tac: "string list -> int -> tactic"} \\ \end{mldecls} \<^descr> \<^ML>\Rule_Insts.res_inst_tac\~\ctxt insts thm i\ instantiates the rule @@ -415,9 +415,9 @@ text %mlref \ \begin{mldecls} - @{index_ML rotate_tac: "int -> int -> tactic"} \\ - @{index_ML distinct_subgoals_tac: tactic} \\ - @{index_ML flexflex_tac: "Proof.context -> tactic"} \\ + @{define_ML rotate_tac: "int -> int -> tactic"} \\ + @{define_ML distinct_subgoals_tac: tactic} \\ + @{define_ML flexflex_tac: "Proof.context -> tactic"} \\ \end{mldecls} \<^descr> \<^ML>\rotate_tac\~\n i\ rotates the premises of subgoal \i\ by \n\ @@ -450,9 +450,9 @@ text %mlref \ \begin{mldecls} - @{index_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\ - @{index_ML Drule.compose: "thm * int * thm -> thm"} \\ - @{index_ML_infix COMP: "thm * thm -> thm"} \\ + @{define_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\ + @{define_ML Drule.compose: "thm * int * thm -> thm"} \\ + @{define_ML_infix COMP: "thm * thm -> thm"} \\ \end{mldecls} \<^descr> \<^ML>\compose_tac\~\ctxt (flag, rule, m) i\ refines subgoal \i\ using @@ -502,17 +502,17 @@ text %mlref \ \begin{mldecls} - @{index_ML_infix "THEN": "tactic * tactic -> tactic"} \\ - @{index_ML_infix "ORELSE": "tactic * tactic -> tactic"} \\ - @{index_ML_infix "APPEND": "tactic * tactic -> tactic"} \\ - @{index_ML "EVERY": "tactic list -> tactic"} \\ - @{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex] + @{define_ML_infix "THEN": "tactic * tactic -> tactic"} \\ + @{define_ML_infix "ORELSE": "tactic * tactic -> tactic"} \\ + @{define_ML_infix "APPEND": "tactic * tactic -> tactic"} \\ + @{define_ML "EVERY": "tactic list -> tactic"} \\ + @{define_ML "FIRST": "tactic list -> tactic"} \\[0.5ex] - @{index_ML_infix "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ - @{index_ML_infix "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ - @{index_ML_infix "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ - @{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\ - @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\ + @{define_ML_infix "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ + @{define_ML_infix "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ + @{define_ML_infix "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ + @{define_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\ + @{define_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\ \end{mldecls} \<^descr> \tac\<^sub>1\~\<^ML_op>\THEN\~\tac\<^sub>2\ is the sequential composition of \tac\<^sub>1\ and @@ -555,11 +555,11 @@ text %mlref \ \begin{mldecls} - @{index_ML "TRY": "tactic -> tactic"} \\ - @{index_ML "REPEAT": "tactic -> tactic"} \\ - @{index_ML "REPEAT1": "tactic -> tactic"} \\ - @{index_ML "REPEAT_DETERM": "tactic -> tactic"} \\ - @{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\ + @{define_ML "TRY": "tactic -> tactic"} \\ + @{define_ML "REPEAT": "tactic -> tactic"} \\ + @{define_ML "REPEAT1": "tactic -> tactic"} \\ + @{define_ML "REPEAT_DETERM": "tactic -> tactic"} \\ + @{define_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\ \end{mldecls} \<^descr> \<^ML>\TRY\~\tac\ applies \tac\ to the goal state and returns the resulting @@ -641,13 +641,13 @@ text %mlref \ \begin{mldecls} - @{index_ML ALLGOALS: "(int -> tactic) -> tactic"} \\ - @{index_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\ - @{index_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\ - @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\ - @{index_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\ - @{index_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\ - @{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\ + @{define_ML ALLGOALS: "(int -> tactic) -> tactic"} \\ + @{define_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\ + @{define_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\ + @{define_ML HEADGOAL: "(int -> tactic) -> tactic"} \\ + @{define_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\ + @{define_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\ + @{define_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\ \end{mldecls} \<^descr> \<^ML>\ALLGOALS\~\tac\ is equivalent to \tac n\~\<^ML_op>\THEN\~\\\~\<^ML_op>\THEN\~\tac 1\. It applies the \tac\ to all the subgoals, counting downwards. @@ -689,8 +689,8 @@ text \ \begin{mldecls} - @{index_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\ - @{index_ML CHANGED: "tactic -> tactic"} \\ + @{define_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\ + @{define_ML CHANGED: "tactic -> tactic"} \\ \end{mldecls} \<^descr> \<^ML>\FILTER\~\sat tac\ applies \tac\ to the goal state and returns a @@ -706,9 +706,9 @@ text \ \begin{mldecls} - @{index_ML DEPTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\ - @{index_ML DEPTH_SOLVE: "tactic -> tactic"} \\ - @{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\ + @{define_ML DEPTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\ + @{define_ML DEPTH_SOLVE: "tactic -> tactic"} \\ + @{define_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\ \end{mldecls} \<^descr> \<^ML>\DEPTH_FIRST\~\sat tac\ returns the goal state if \sat\ returns true. @@ -729,9 +729,9 @@ text \ \begin{mldecls} - @{index_ML BREADTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\ - @{index_ML BEST_FIRST: "(thm -> bool) * (thm -> int) -> tactic -> tactic"} \\ - @{index_ML THEN_BEST_FIRST: "tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic"} \\ + @{define_ML BREADTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\ + @{define_ML BEST_FIRST: "(thm -> bool) * (thm -> int) -> tactic -> tactic"} \\ + @{define_ML THEN_BEST_FIRST: "tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic"} \\ \end{mldecls} These search strategies will find a solution if one exists. However, they do @@ -763,10 +763,10 @@ text \ \begin{mldecls} - @{index_ML COND: "(thm -> bool) -> tactic -> tactic -> tactic"} \\ - @{index_ML IF_UNSOLVED: "tactic -> tactic"} \\ - @{index_ML SOLVE: "tactic -> tactic"} \\ - @{index_ML DETERM: "tactic -> tactic"} \\ + @{define_ML COND: "(thm -> bool) -> tactic -> tactic -> tactic"} \\ + @{define_ML IF_UNSOLVED: "tactic -> tactic"} \\ + @{define_ML SOLVE: "tactic -> tactic"} \\ + @{define_ML DETERM: "tactic -> tactic"} \\ \end{mldecls} \<^descr> \<^ML>\COND\~\sat tac\<^sub>1 tac\<^sub>2\ applies \tac\<^sub>1\ to the goal state if it @@ -792,10 +792,10 @@ text \ \begin{mldecls} - @{index_ML has_fewer_prems: "int -> thm -> bool"} \\ - @{index_ML Thm.eq_thm: "thm * thm -> bool"} \\ - @{index_ML Thm.eq_thm_prop: "thm * thm -> bool"} \\ - @{index_ML size_of_thm: "thm -> int"} \\ + @{define_ML has_fewer_prems: "int -> thm -> bool"} \\ + @{define_ML Thm.eq_thm: "thm * thm -> bool"} \\ + @{define_ML Thm.eq_thm_prop: "thm * thm -> bool"} \\ + @{define_ML size_of_thm: "thm -> int"} \\ \end{mldecls} \<^descr> \<^ML>\has_fewer_prems\~\n thm\ reports whether \thm\ has fewer than \n\ diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Isar_Ref/Generic.thy --- a/src/Doc/Isar_Ref/Generic.thy Sat May 22 13:35:25 2021 +0200 +++ b/src/Doc/Isar_Ref/Generic.thy Sat May 22 21:52:13 2021 +0200 @@ -638,7 +638,7 @@ of the term ordering. The default is lexicographic ordering of term structure, but this could be - also changed locally for special applications via @{index_ML + also changed locally for special applications via @{define_ML Simplifier.set_term_ord} in Isabelle/ML. \<^medskip> @@ -866,9 +866,9 @@ text \ \begin{mldecls} - @{index_ML Simplifier.set_subgoaler: "(Proof.context -> int -> tactic) -> + @{define_ML Simplifier.set_subgoaler: "(Proof.context -> int -> tactic) -> Proof.context -> Proof.context"} \\ - @{index_ML Simplifier.prems_of: "Proof.context -> thm list"} \\ + @{define_ML Simplifier.prems_of: "Proof.context -> thm list"} \\ \end{mldecls} The subgoaler is the tactic used to solve subgoals arising out of @@ -906,13 +906,13 @@ text \ \begin{mldecls} - @{index_ML_type solver} \\ - @{index_ML Simplifier.mk_solver: "string -> + @{define_ML_type solver} \\ + @{define_ML Simplifier.mk_solver: "string -> (Proof.context -> int -> tactic) -> solver"} \\ - @{index_ML_infix setSolver: "Proof.context * solver -> Proof.context"} \\ - @{index_ML_infix addSolver: "Proof.context * solver -> Proof.context"} \\ - @{index_ML_infix setSSolver: "Proof.context * solver -> Proof.context"} \\ - @{index_ML_infix addSSolver: "Proof.context * solver -> Proof.context"} \\ + @{define_ML_infix setSolver: "Proof.context * solver -> Proof.context"} \\ + @{define_ML_infix addSolver: "Proof.context * solver -> Proof.context"} \\ + @{define_ML_infix setSSolver: "Proof.context * solver -> Proof.context"} \\ + @{define_ML_infix addSSolver: "Proof.context * solver -> Proof.context"} \\ \end{mldecls} A solver is a tactic that attempts to solve a subgoal after simplification. @@ -992,17 +992,17 @@ text \ \begin{mldecls} - @{index_ML_infix setloop: "Proof.context * + @{define_ML_infix setloop: "Proof.context * (Proof.context -> int -> tactic) -> Proof.context"} \\ - @{index_ML_infix addloop: "Proof.context * + @{define_ML_infix addloop: "Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\ - @{index_ML_infix delloop: "Proof.context * string -> Proof.context"} \\ - @{index_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\ - @{index_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\ - @{index_ML Splitter.add_split_bang: " + @{define_ML_infix delloop: "Proof.context * string -> Proof.context"} \\ + @{define_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\ + @{define_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\ + @{define_ML Splitter.add_split_bang: " thm -> Proof.context -> Proof.context"} \\ - @{index_ML Splitter.del_split: "thm -> Proof.context -> Proof.context"} \\ + @{define_ML Splitter.del_split: "thm -> Proof.context -> Proof.context"} \\ \end{mldecls} The looper is a list of tactics that are applied after simplification, in @@ -1624,23 +1624,23 @@ text \ \begin{mldecls} - @{index_ML_type wrapper = "(int -> tactic) -> (int -> tactic)"} \\[0.5ex] - @{index_ML_infix addSWrapper: "Proof.context * + @{define_ML_type wrapper = "(int -> tactic) -> (int -> tactic)"} \\[0.5ex] + @{define_ML_infix addSWrapper: "Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context"} \\ - @{index_ML_infix addSbefore: "Proof.context * + @{define_ML_infix addSbefore: "Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\ - @{index_ML_infix addSafter: "Proof.context * + @{define_ML_infix addSafter: "Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\ - @{index_ML_infix delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex] - @{index_ML_infix addWrapper: "Proof.context * + @{define_ML_infix delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex] + @{define_ML_infix addWrapper: "Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context"} \\ - @{index_ML_infix addbefore: "Proof.context * + @{define_ML_infix addbefore: "Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\ - @{index_ML_infix addafter: "Proof.context * + @{define_ML_infix addafter: "Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\ - @{index_ML_infix delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex] - @{index_ML addSss: "Proof.context -> Proof.context"} \\ - @{index_ML addss: "Proof.context -> Proof.context"} \\ + @{define_ML_infix delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex] + @{define_ML addSss: "Proof.context -> Proof.context"} \\ + @{define_ML addss: "Proof.context -> Proof.context"} \\ \end{mldecls} The proof strategy of the Classical Reasoner is simple. Perform as diff -r eccc4a13216d -r 35d8132633c6 src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sat May 22 13:35:25 2021 +0200 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sat May 22 21:52:13 2021 +0200 @@ -220,8 +220,8 @@ text \ \begin{mldecls} - @{index_ML print_mode_value: "unit -> string list"} \\ - @{index_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\ + @{define_ML print_mode_value: "unit -> string list"} \\ + @{define_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\ \end{mldecls} The \<^emph>\print mode\ facility allows to modify various operations for printing. diff -r eccc4a13216d -r 35d8132633c6 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Sat May 22 13:35:25 2021 +0200 +++ b/src/Doc/antiquote_setup.ML Sat May 22 21:52:13 2021 +0200 @@ -111,12 +111,12 @@ val _ = Theory.setup - (antiquotation_ml' parse_ml test_val "" \<^binding>\index_ML\ #> - antiquotation_ml' parse_ml test_op "infix" \<^binding>\index_ML_infix\ #> - antiquotation_ml' parse_type test_type "type" \<^binding>\index_ML_type\ #> - antiquotation_ml' parse_exn text_exn "exception" \<^binding>\index_ML_exception\ #> - antiquotation_ml' parse_struct test_struct "structure" \<^binding>\index_ML_structure\ #> - antiquotation_ml' parse_struct test_functor "functor" \<^binding>\index_ML_functor\); + (antiquotation_ml' parse_ml test_val "" \<^binding>\define_ML\ #> + antiquotation_ml' parse_ml test_op "infix" \<^binding>\define_ML_infix\ #> + antiquotation_ml' parse_type test_type "type" \<^binding>\define_ML_type\ #> + antiquotation_ml' parse_exn text_exn "exception" \<^binding>\define_ML_exception\ #> + antiquotation_ml' parse_struct test_struct "structure" \<^binding>\define_ML_structure\ #> + antiquotation_ml' parse_struct test_functor "functor" \<^binding>\define_ML_functor\); end;