diff -r 151f894984d8 -r 2bf52eec4e8a src/Doc/Implementation/Isar.thy --- a/src/Doc/Implementation/Isar.thy Wed Oct 14 15:06:42 2015 +0200 +++ b/src/Doc/Implementation/Isar.thy Wed Oct 14 15:10:32 2015 +0200 @@ -81,7 +81,7 @@ \begin{description} - \item Type @{ML_type Proof.state} represents Isar proof states. + \<^descr> Type @{ML_type Proof.state} represents Isar proof states. This is a block-structured configuration with proof context, linguistic mode, and optional goal. The latter consists of goal context, goal facts (``@{text "using"}''), and tactical goal state @@ -91,7 +91,7 @@ refinement of some parts of the tactical goal --- how exactly is defined by the proof method that is applied in that situation. - \item @{ML Proof.assert_forward}, @{ML Proof.assert_chain}, @{ML + \<^descr> @{ML Proof.assert_forward}, @{ML Proof.assert_chain}, @{ML Proof.assert_backward} are partial identity functions that fail unless a certain linguistic mode is active, namely ``@{text "proof(state)"}'', ``@{text "proof(chain)"}'', ``@{text @@ -101,24 +101,24 @@ It is advisable study the implementations of existing proof commands for suitable modes to be asserted. - \item @{ML Proof.simple_goal}~@{text "state"} returns the structured + \<^descr> @{ML Proof.simple_goal}~@{text "state"} returns the structured Isar goal (if available) in the form seen by ``simple'' methods (like @{method simp} or @{method blast}). The Isar goal facts are already inserted as premises into the subgoals, which are presented individually as in @{ML Proof.goal}. - \item @{ML Proof.goal}~@{text "state"} returns the structured Isar + \<^descr> @{ML Proof.goal}~@{text "state"} returns the structured Isar goal (if available) in the form seen by regular methods (like @{method rule}). The auxiliary internal encoding of Pure conjunctions is split into individual subgoals as usual. - \item @{ML Proof.raw_goal}~@{text "state"} returns the structured + \<^descr> @{ML Proof.raw_goal}~@{text "state"} returns the structured Isar goal (if available) in the raw internal form seen by ``raw'' methods (like @{method induct}). This form is rarely appropriate for diagnostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal} should be used in most situations. - \item @{ML Proof.theorem}~@{text "before_qed after_qed statement ctxt"} + \<^descr> @{ML Proof.theorem}~@{text "before_qed after_qed statement ctxt"} initializes a toplevel Isar proof state within a given context. The optional @{text "before_qed"} method is applied at the end of @@ -150,7 +150,7 @@ \begin{description} - \item @{text "@{Isar.goal}"} refers to the regular goal state (if + \<^descr> @{text "@{Isar.goal}"} refers to the regular goal state (if available) of the current proof state managed by the Isar toplevel --- as abstract value. @@ -320,33 +320,33 @@ \begin{description} - \item Type @{ML_type Proof.method} represents proof methods as + \<^descr> Type @{ML_type Proof.method} represents proof methods as abstract type. - \item @{ML METHOD_CASES}~@{text "(fn facts => cases_tactic)"} wraps + \<^descr> @{ML METHOD_CASES}~@{text "(fn facts => cases_tactic)"} wraps @{text cases_tactic} depending on goal facts as proof method with cases; the goal context is passed via method syntax. - \item @{ML METHOD}~@{text "(fn facts => tactic)"} wraps @{text + \<^descr> @{ML METHOD}~@{text "(fn facts => tactic)"} wraps @{text tactic} depending on goal facts as regular proof method; the goal context is passed via method syntax. - \item @{ML SIMPLE_METHOD}~@{text "tactic"} wraps a tactic that + \<^descr> @{ML SIMPLE_METHOD}~@{text "tactic"} wraps a tactic that addresses all subgoals uniformly as simple proof method. Goal facts are already inserted into all subgoals before @{text "tactic"} is applied. - \item @{ML SIMPLE_METHOD'}~@{text "tactic"} wraps a tactic that + \<^descr> @{ML SIMPLE_METHOD'}~@{text "tactic"} wraps a tactic that addresses a specific subgoal as simple proof method that operates on subgoal 1. Goal facts are inserted into the subgoal then the @{text "tactic"} is applied. - \item @{ML Method.insert_tac}~@{text "facts i"} inserts @{text + \<^descr> @{ML Method.insert_tac}~@{text "facts i"} inserts @{text "facts"} into subgoal @{text "i"}. This is convenient to reproduce part of the @{ML SIMPLE_METHOD} or @{ML SIMPLE_METHOD'} wrapping within regular @{ML METHOD}, for example. - \item @{ML Method.setup}~@{text "name parser description"} provides + \<^descr> @{ML Method.setup}~@{text "name parser description"} provides the functionality of the Isar command @{command method_setup} as ML function. @@ -548,17 +548,17 @@ \begin{description} - \item Type @{ML_type attribute} represents attributes as concrete + \<^descr> Type @{ML_type attribute} represents attributes as concrete type alias. - \item @{ML Thm.rule_attribute}~@{text "(fn context => rule)"} wraps + \<^descr> @{ML Thm.rule_attribute}~@{text "(fn context => rule)"} wraps a context-dependent rule (mapping on @{ML_type thm}) as attribute. - \item @{ML Thm.declaration_attribute}~@{text "(fn thm => decl)"} + \<^descr> @{ML Thm.declaration_attribute}~@{text "(fn thm => decl)"} wraps a theorem-dependent declaration (mapping on @{ML_type Context.generic}) as attribute. - \item @{ML Attrib.setup}~@{text "name parser description"} provides + \<^descr> @{ML Attrib.setup}~@{text "name parser description"} provides the functionality of the Isar command @{command attribute_setup} as ML function. @@ -576,7 +576,7 @@ \begin{description} - \item @{text "@{attributes [\]}"} embeds attribute source + \<^descr> @{text "@{attributes [\]}"} embeds attribute source representation into the ML text, which is particularly useful with declarations like @{ML Local_Theory.note}. Attribute names are internalized at compile time, but the source is unevaluated. This