src/HOL/Extraction.thy
changeset 34913 d8cb720c9c53
parent 33723 14d0dadd9517
child 37233 b78f31ca4675
     1.1 --- a/src/HOL/Extraction.thy	Sun Jan 10 18:37:37 2010 +0100
     1.2 +++ b/src/HOL/Extraction.thy	Sun Jan 10 18:39:50 2010 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Extraction.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Stefan Berghofer, TU Muenchen
     1.7  *)
     1.8  
     1.9 @@ -28,11 +27,13 @@
    1.10    allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
    1.11    notE' impE' impE iffE imp_cong simp_thms eq_True eq_False
    1.12    induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
    1.13 -  induct_atomize induct_rulify induct_rulify_fallback
    1.14 +  induct_atomize induct_atomize' induct_rulify induct_rulify'
    1.15 +  induct_rulify_fallback induct_trueI
    1.16    True_implies_equals TrueE
    1.17  
    1.18  lemmas [extraction_expand_def] =
    1.19    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    1.20 +  induct_true_def induct_false_def
    1.21  
    1.22  datatype sumbool = Left | Right
    1.23