equal
deleted
inserted
replaced
108 nitpick [dont_specialize, expect = none] |
108 nitpick [dont_specialize, expect = none] |
109 sorry |
109 sorry |
110 |
110 |
111 lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}. |
111 lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}. |
112 f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x" |
112 f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x" |
113 nitpick [expect = potential] (* unfortunate *) |
113 nitpick [expect = genuine] |
114 oops |
114 oops |
115 |
115 |
116 lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}. |
116 lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}. |
117 f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x" |
117 f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x" |
118 nitpick [expect = potential] (* unfortunate *) |
118 nitpick [expect = genuine] |
119 oops |
119 oops |
120 |
120 |
121 lemma "\<forall>a. g a = a |
121 lemma "\<forall>a. g a = a |
122 \<Longrightarrow> \<exists>one \<in> {1}. \<exists>two \<in> {2}. f5 g x = |
122 \<Longrightarrow> \<exists>one \<in> {1}. \<exists>two \<in> {2}. f5 g x = |
123 f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x" |
123 f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x" |