# 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%