author | berghofe |
Thu, 01 May 2003 08:39:37 +0200 | |
changeset 13942 | dc93e3a68142 |
parent 13941 | 2ae108fcd068 |
child 13943 | 83d842ccd4aa |
--- a/src/HOL/Extraction.thy Wed Apr 30 18:33:41 2003 +0200 +++ b/src/HOL/Extraction.thy Thu May 01 08:39:37 2003 +0200 @@ -52,7 +52,7 @@ allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 notE' impE' impE iffE imp_cong simp_thms induct_forall_eq induct_implies_eq induct_equal_eq - induct_forall_def induct_implies_def + induct_forall_def induct_implies_def induct_impliesI induct_atomize induct_rulify1 induct_rulify2 datatype sumbool = Left | Right