equal
deleted
inserted
replaced
925 have "\<And>x::'a star. ( *f* (\<lambda>x. 1)) x = 1" |
925 have "\<And>x::'a star. ( *f* (\<lambda>x. 1)) x = 1" |
926 by transfer simp |
926 by transfer simp |
927 then show ?case by simp |
927 then show ?case by simp |
928 next |
928 next |
929 case (Suc n) |
929 case (Suc n) |
930 have "\<And>x::'a star. x * ( *f* (\<lambda>x\<Colon>'a. x ^ n)) x = ( *f* (\<lambda>x\<Colon>'a. x * x ^ n)) x" |
930 have "\<And>x::'a star. x * ( *f* (\<lambda>x::'a. x ^ n)) x = ( *f* (\<lambda>x::'a. x * x ^ n)) x" |
931 by transfer simp |
931 by transfer simp |
932 with Suc show ?case by simp |
932 with Suc show ?case by simp |
933 qed |
933 qed |
934 qed |
934 qed |
935 |
935 |