# HG changeset patch # User bulwahn # Date 1324474701 -3600 # Node ID e586f6d136b7b0aa1b4afed3f3e8620e9ab4ceac # Parent 8c4a5e664fbc86ddd91e3d4e6c4e76b8f4b6d865 added some basic documentation about method induction_schema extracted from old NEWS diff -r 8c4a5e664fbc -r e586f6d136b7 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Dec 21 14:24:29 2011 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Dec 21 14:38:21 2011 +0100 @@ -493,6 +493,7 @@ @{method_def (HOL) relation} & : & @{text method} \\ @{method_def (HOL) lexicographic_order} & : & @{text method} \\ @{method_def (HOL) size_change} & : & @{text method} \\ + @{method_def (HOL) induction_schema} & : & @{text method} \\ \end{matharray} @{rail " @@ -502,6 +503,8 @@ ; @@{method (HOL) size_change} ( orders (@{syntax clasimpmod} * ) ) ; + @@{method (HOL) induction_schema} + ; orders: ( 'max' | 'min' | 'ms' ) * "} @@ -541,6 +544,12 @@ For local descent proofs, the @{syntax clasimpmod} modifiers are accepted (as for @{method auto}). + \item @{method (HOL) induction_schema} derives user-specified + induction rules from well-founded induction and completeness of + patterns. This factors out some operations that are done internally + by the function package and makes them available separately. See + @{file "~~/src/HOL/ex/Induction_Schema.thy"} for examples. + \end{description} *} diff -r 8c4a5e664fbc -r e586f6d136b7 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Dec 21 14:24:29 2011 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Dec 21 14:38:21 2011 +0100 @@ -707,6 +707,7 @@ \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\ \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}} & : & \isa{method} \\ \indexdef{HOL}{method}{size\_change}\hypertarget{method.HOL.size-change}{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}} & : & \isa{method} \\ + \indexdef{HOL}{method}{induction\_schema}\hypertarget{method.HOL.induction-schema}{\hyperlink{method.HOL.induction-schema}{\mbox{\isa{induction{\isaliteral{5F}{\isacharunderscore}}schema}}}} & : & \isa{method} \\ \end{matharray} \begin{railoutput} @@ -729,6 +730,9 @@ \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[] \rail@endplus \rail@end +\rail@begin{1}{} +\rail@term{\hyperlink{method.HOL.induction-schema}{\mbox{\isa{induction{\isaliteral{5F}{\isacharunderscore}}schema}}}}[] +\rail@end \rail@begin{4}{\isa{orders}} \rail@plus \rail@nextplus{1} @@ -779,6 +783,12 @@ For local descent proofs, the \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}} modifiers are accepted (as for \hyperlink{method.auto}{\mbox{\isa{auto}}}). + \item \hyperlink{method.HOL.induction-schema}{\mbox{\isa{induction{\isaliteral{5F}{\isacharunderscore}}schema}}} derives user-specified + induction rules from well-founded induction and completeness of + patterns. This factors out some operations that are done internally + by the function package and makes them available separately. See + \verb|~~/src/HOL/ex/Induction_Schema.thy| for examples. + \end{description}% \end{isamarkuptext}% \isamarkuptrue%