equal
deleted
inserted
replaced
56 by (rule eq_reflection) (rule if_bool_eq_conj) |
56 by (rule eq_reflection) (rule if_bool_eq_conj) |
57 |
57 |
58 lemma Ex1_def [nitpick_def, no_atp]: |
58 lemma Ex1_def [nitpick_def, no_atp]: |
59 "Ex1 P \<equiv> \<exists>x. P = {x}" |
59 "Ex1 P \<equiv> \<exists>x. P = {x}" |
60 apply (rule eq_reflection) |
60 apply (rule eq_reflection) |
61 apply (simp add: Ex1_def set_ext_iff) |
61 apply (simp add: Ex1_def set_eq_iff) |
62 apply (rule iffI) |
62 apply (rule iffI) |
63 apply (erule exE) |
63 apply (erule exE) |
64 apply (erule conjE) |
64 apply (erule conjE) |
65 apply (rule_tac x = x in exI) |
65 apply (rule_tac x = x in exI) |
66 apply (rule allI) |
66 apply (rule allI) |