# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID e89c7ac4ce16d7dfd9529314fa40aae4d5a0019c
# Parent  0dcd3a623a6ef2038b139a7eca15b55d258557a2
documented extraction plugin

diff -r 0dcd3a623a6e -r e89c7ac4ce16 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -2932,6 +2932,17 @@
 *}
 
 
+subsection {* Program Extraction
+  \label{ssec:program-extraction} *}
+
+text {*
+The \hthm{extraction} plugin provides realizers for induction and case analysis,
+to enable program extraction from proofs involving datatypes. This functionality
+is only available with full proof objects, i.e., with the @{text "HOL-Proofs"}
+session.
+*}
+
+
 (*
 section {* Known Bugs and Limitations
   \label{sec:known-bugs-and-limitations} *}