# HG changeset patch
# User berghofe
# Date 1263145190 -3600
# Node ID d8cb720c9c5395738077488841715d5fea1936e1
# Parent  c04747153bcf35c99c24943a8d211d1b5f09d142
Expand proofs of induct_atomize'/rulify'.

diff -r c04747153bcf -r d8cb720c9c53 src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Sun Jan 10 18:37:37 2010 +0100
+++ b/src/HOL/Extraction.thy	Sun Jan 10 18:39:50 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Extraction.thy
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 *)
 
@@ -28,11 +27,13 @@
   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_atomize induct_rulify induct_rulify_fallback
+  induct_atomize induct_atomize' induct_rulify induct_rulify'
+  induct_rulify_fallback induct_trueI
   True_implies_equals TrueE
 
 lemmas [extraction_expand_def] =
   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
+  induct_true_def induct_false_def
 
 datatype sumbool = Left | Right