--- a/src/HOL/Extraction.thy Sun Nov 15 20:57:42 2009 +0100
+++ b/src/HOL/Extraction.thy Sun Nov 15 21:58:40 2009 +0100
@@ -43,10 +43,12 @@
allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
notE' impE' impE iffE imp_cong simp_thms eq_True eq_False
induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
- induct_forall_def induct_implies_def induct_equal_def induct_conj_def
induct_atomize induct_rulify induct_rulify_fallback
True_implies_equals TrueE
+lemmas [extraction_expand_def] =
+ induct_forall_def induct_implies_def induct_equal_def induct_conj_def
+
datatype sumbool = Left | Right
subsection {* Type of extracted program *}