diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Implementation/Logic.thy Fri Oct 16 14:53:26 2015 +0200 @@ -138,8 +138,6 @@ @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type class} represents type classes. \<^descr> Type @{ML_type sort} represents sorts, i.e.\ finite @@ -185,8 +183,6 @@ \<^descr> @{ML Sign.primitive_arity}~@{text "(\, \<^vec>s, s)"} declares the arity @{text "\ :: (\<^vec>s)s"}. - - \end{description} \ text %mlantiq \ @@ -211,8 +207,6 @@ @@{ML_antiquotation typ} type \} - \begin{description} - \<^descr> @{text "@{class c}"} inlines the internalized class @{text "c"} --- as @{ML_type string} literal. @@ -231,8 +225,6 @@ \<^descr> @{text "@{typ \}"} inlines the internalized type @{text "\"} --- as constructor term for datatype @{ML_type typ}. - - \end{description} \ @@ -383,8 +375,6 @@ @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\ \end{mldecls} - \begin{description} - \<^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 @@ -440,8 +430,6 @@ Sign.const_instance}~@{text "thy (c, [\\<^sub>1, \, \\<^sub>n])"} convert between two representations of polymorphic constants: full type instance vs.\ compact type arguments form. - - \end{description} \ text %mlantiq \ @@ -464,8 +452,6 @@ @@{ML_antiquotation prop} prop \} - \begin{description} - \<^descr> @{text "@{const_name c}"} inlines the internalized logical constant name @{text "c"} --- as @{ML_type string} literal. @@ -483,8 +469,6 @@ \<^descr> @{text "@{prop \}"} inlines the internalized proposition @{text "\"} --- as constructor term for datatype @{ML_type term}. - - \end{description} \ @@ -681,8 +665,6 @@ Defs.entry -> Defs.entry list -> theory -> theory"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Thm.peek_status}~@{text "thm"} informs about the current status of the derivation object behind the given theorem. This is a snapshot of a potentially ongoing (parallel) evaluation of proofs. @@ -778,8 +760,6 @@ declares dependencies of a named specification for constant @{text "c\<^sub>\"}, relative to existing specifications for constants @{text "\<^vec>d\<^sub>\"}. This also works for type constructors. - - \end{description} \ @@ -808,8 +788,6 @@ @'by' method method? \} - \begin{description} - \<^descr> @{text "@{ctyp \}"} produces a certified type wrt.\ the current background theory --- as abstract value of type @{ML_type ctyp}. @@ -840,9 +818,6 @@ "by"} step. More complex Isar proofs should be done in regular theory source, before compiling the corresponding ML text that uses the result. - - \end{description} - \ @@ -915,8 +890,6 @@ @{index_ML Logic.dest_type: "term -> typ"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Conjunction.intr} derives @{text "A &&& B"} from @{text "A"} and @{text "B"}. @@ -933,8 +906,6 @@ \<^descr> @{ML Logic.dest_type}~@{text "TYPE(\)"} recovers the type @{text "\"}. - - \end{description} \ @@ -972,16 +943,12 @@ @{index_ML Thm.strip_shyps: "thm -> thm"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Thm.extra_shyps}~@{text "thm"} determines the extraneous sort hypotheses of the given theorem, i.e.\ the sorts that are not present within type variables of the statement. \<^descr> @{ML Thm.strip_shyps}~@{text "thm"} removes any extraneous sort hypotheses that can be witnessed from the type signature. - - \end{description} \ text %mlex \The following artificial example demonstrates the @@ -1069,8 +1036,6 @@ Regular user-level inferences in Isabelle/Pure always maintain the following canonical form of results: - \begin{itemize} - \<^item> Normalization by @{text "(A \ (\x. B x)) \ (\x. A \ B x)"}, which is a theorem of Pure, means that quantifiers are pushed in front of implication at each level of nesting. The normal form is a @@ -1081,8 +1046,6 @@ \ A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \ A ?\<^vec>x"}. Note that this representation looses information about the order of parameters, and vacuous quantifiers vanish automatically. - - \end{itemize} \ text %mlref \ @@ -1090,14 +1053,10 @@ @{index_ML Simplifier.norm_hhf: "Proof.context -> thm -> thm"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Simplifier.norm_hhf}~@{text "ctxt thm"} normalizes the given theorem according to the canonical form specified above. This is occasionally helpful to repair some low-level tools that do not handle Hereditary Harrop Formulae properly. - - \end{description} \ @@ -1174,8 +1133,6 @@ @{index_ML_op "OF": "thm * thm list -> thm"} \\ \end{mldecls} - \begin{description} - \<^descr> @{text "rule\<^sub>1 RSN (i, rule\<^sub>2)"} resolves the conclusion of @{text "rule\<^sub>1"} with the @{text i}-th premise of @{text "rule\<^sub>2"}, according to the @{inference resolution} principle explained above. @@ -1211,8 +1168,6 @@ This corresponds to the rule attribute @{attribute OF} in Isar source language. - - \end{description} \ @@ -1359,8 +1314,6 @@ @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type proof} represents proof terms; this is a datatype with constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_op "%"}, @{index_ML_op "%%"}, @{index_ML PBound}, @@ -1417,8 +1370,6 @@ \<^descr> @{ML Proof_Syntax.pretty_proof}~@{text "ctxt prf"} pretty-prints the given proof term. - - \end{description} \ text %mlex \Detailed proof information of a theorem may be retrieved