author | berghofe |

Thu May 01 08:39:37 2003 +0200 (2003-05-01) | |

changeset 13942 | dc93e3a68142 |

parent 13941 | 2ae108fcd068 |

child 13943 | 83d842ccd4aa |

induct_impliesI is now unfolded.

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