src/HOL/Induct/Com.thy
changeset 61424 c3658c18b7bc
parent 60530 44f9873d6f6f
child 63167 0909deb8059b
     1.1 --- a/src/HOL/Induct/Com.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Induct/Com.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -139,7 +139,7 @@
     1.4  text\<open>Make the induction rule look nicer -- though @{text eta_contract} makes the new
     1.5      version look worse than it is...\<close>
     1.6  
     1.7 -lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
     1.8 +lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (case_prod (%v. case_prod (case_prod P v)))"
     1.9    by auto
    1.10  
    1.11  text\<open>New induction rule.  Note the form of the VALOF induction hypothesis\<close>