induct_impliesI is now unfolded.
authorberghofe
Thu May 01 08:39:37 2003 +0200 (2003-05-01)
changeset 13942dc93e3a68142
parent 13941 2ae108fcd068
child 13943 83d842ccd4aa
induct_impliesI is now unfolded.
src/HOL/Extraction.thy
     1.1 --- a/src/HOL/Extraction.thy	Wed Apr 30 18:33:41 2003 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Thu May 01 08:39:37 2003 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4    allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
     1.5    notE' impE' impE iffE imp_cong simp_thms
     1.6    induct_forall_eq induct_implies_eq induct_equal_eq
     1.7 -  induct_forall_def induct_implies_def
     1.8 +  induct_forall_def induct_implies_def induct_impliesI
     1.9    induct_atomize induct_rulify1 induct_rulify2
    1.10  
    1.11  datatype sumbool = Left | Right