| changeset 67613 | ce654b0e6d69 |
| parent 61933 | cf58b5b794b2 |
| child 69597 | ff784d5a5bfb |
| 67610:4939494ed791 | 67613:ce654b0e6d69 |
|---|---|
74 ~(c | (~p & (p | (q & ~q)))) |] ==> False" |
74 ~(c | (~p & (p | (q & ~q)))) |] ==> False" |
75 by satx |
75 by satx |
76 |
76 |
77 text \<open>eta-Equivalence\<close> |
77 text \<open>eta-Equivalence\<close> |
78 |
78 |
79 lemma "(ALL x. P x) | ~ All P" |
79 lemma "(\<forall>x. P x) \<or> \<not> All P" |
80 by sat |
80 by sat |
81 |
81 |
82 declare [[sat_trace = false]] |
82 declare [[sat_trace = false]] |
83 declare [[quick_and_dirty = false]] |
83 declare [[quick_and_dirty = false]] |
84 |
84 |