| changeset 34120 | f9920a3ddf50 |
| parent 32968 | c9fbd4a4d39e |
| child 35315 | fbdc860d87a3 |
--- a/src/HOL/ex/Refute_Examples.thy Mon Dec 14 11:01:04 2009 +0100 +++ b/src/HOL/ex/Refute_Examples.thy Mon Dec 14 12:14:12 2009 +0100 @@ -1516,6 +1516,17 @@ refute oops +text {* Structured proofs *} + +lemma "x = y" +proof cases + assume "x = y" + show ?thesis + refute + refute [no_assms] + refute [no_assms = false] +oops + refute_params [satsolver="auto"] end