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