summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/HOL.thy

changeset 13598 | 8bc77b17f59f |

parent 13596 | ee5f79b210c1 |

child 13638 | 2b234b079245 |

1.1 --- a/src/HOL/HOL.thy Mon Sep 30 15:45:11 2002 +0200 1.2 +++ b/src/HOL/HOL.thy Mon Sep 30 16:09:05 2002 +0200 1.3 @@ -549,8 +549,14 @@ 1.4 induct_conj (induct_implies C A) (induct_implies C B)" 1.5 by (unfold induct_implies_def induct_conj_def) rules 1.6 1.7 -lemma induct_conj_curry: "(induct_conj A B ==> C) == (A ==> B ==> C)" 1.8 - by (simp only: atomize_imp atomize_eq induct_conj_def) (rules intro: equal_intr_rule) 1.9 +lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)" 1.10 +proof 1.11 + assume r: "induct_conj A B ==> PROP C" and A B 1.12 + show "PROP C" by (rule r) (simp! add: induct_conj_def) 1.13 +next 1.14 + assume r: "A ==> B ==> PROP C" and "induct_conj A B" 1.15 + show "PROP C" by (rule r) (simp! add: induct_conj_def)+ 1.16 +qed 1.17 1.18 lemma induct_impliesI: "(A ==> B) ==> induct_implies A B" 1.19 by (simp add: induct_implies_def)