src/HOL/ex/Refute_Examples.thy
changeset 36319 8feb2c4bef1a
parent 36131 64b6374a21a8
child 37388 793618618f78
     1.1 --- a/src/HOL/ex/Refute_Examples.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/HOL/ex/Refute_Examples.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -347,12 +347,12 @@
     1.4  
     1.5  subsubsection {* Schematic variables *}
     1.6  
     1.7 -lemma "?P"
     1.8 +schematic_lemma "?P"
     1.9    refute
    1.10    apply auto
    1.11  done
    1.12  
    1.13 -lemma "x = ?y"
    1.14 +schematic_lemma "x = ?y"
    1.15    refute
    1.16    apply auto
    1.17  done