equal
deleted
inserted
replaced
43 |
43 |
44 lemma "\<exists>!x. x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A" |
44 lemma "\<exists>!x. x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A" |
45 nitpick [expect = none] |
45 nitpick [expect = none] |
46 nitpick [card 'a = 1\<emdash>50, expect = none] |
46 nitpick [card 'a = 1\<emdash>50, expect = none] |
47 (* sledgehammer *) |
47 (* sledgehammer *) |
48 sledgehammer |
|
49 by (metis the_equality) |
48 by (metis the_equality) |
50 |
49 |
51 subsection {* 2.4. Skolemization *} |
50 subsection {* 2.4. Skolemization *} |
52 |
51 |
53 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x" |
52 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x" |