Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed problem with induct_conj_curry: variable C should have type prop.
authorberghofe
Mon, 30 Sep 2002 16:09:05 +0200
changeset 13598 8bc77b17f59f
parent 13597 a8230e035e96
child 13599 cfdf7e4cd0d2
Fixed problem with induct_conj_curry: variable C should have type prop.
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOL.thy	Mon Sep 30 15:45:11 2002 +0200
+++ b/src/HOL/HOL.thy	Mon Sep 30 16:09:05 2002 +0200
@@ -549,8 +549,14 @@
     induct_conj (induct_implies C A) (induct_implies C B)"
   by (unfold induct_implies_def induct_conj_def) rules
 
-lemma induct_conj_curry: "(induct_conj A B ==> C) == (A ==> B ==> C)"
-  by (simp only: atomize_imp atomize_eq induct_conj_def) (rules intro: equal_intr_rule)
+lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
+proof
+  assume r: "induct_conj A B ==> PROP C" and A B
+  show "PROP C" by (rule r) (simp! add: induct_conj_def)
+next
+  assume r: "A ==> B ==> PROP C" and "induct_conj A B"
+  show "PROP C" by (rule r) (simp! add: induct_conj_def)+
+qed
 
 lemma induct_impliesI: "(A ==> B) ==> induct_implies A B"
   by (simp add: induct_implies_def)
isabelle