
diff -r ff8b2ac0134c -r f9920a3ddf50 src/HOL/ex/Refute_Examples.thy
--- 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




