| changeset 61337 | 4645502c3c64 |
| parent 59987 | fbe93138e540 |
| child 61343 | 5b5656a63bd6 |
--- a/src/HOL/ex/Refute_Examples.thy Tue Oct 06 13:31:44 2015 +0200 +++ b/src/HOL/ex/Refute_Examples.thy Tue Oct 06 15:14:28 2015 +0200 @@ -332,11 +332,11 @@ subsubsection {* Schematic variables *} -schematic_lemma "?P" +schematic_goal "?P" refute [expect = none] by auto -schematic_lemma "x = ?y" +schematic_goal "x = ?y" refute [expect = none] by auto