src/HOL/ex/set.thy
changeset 36319 8feb2c4bef1a
parent 34055 fdf294ee08b2
child 40928 ace26e2cee91
     1.1 --- a/src/HOL/ex/set.thy	Fri Apr 23 23:33:48 2010 +0200
     1.2 +++ b/src/HOL/ex/set.thy	Fri Apr 23 23:35:43 2010 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    Trivial example of term synthesis: apparently hard for some provers!
     1.5  *}
     1.6  
     1.7 -lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
     1.8 +schematic_lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
     1.9    by blast
    1.10  
    1.11  
    1.12 @@ -60,15 +60,15 @@
    1.13    -- {* Requires best-first search because it is undirectional. *}
    1.14    by best
    1.15  
    1.16 -lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
    1.17 +schematic_lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
    1.18    -- {*This form displays the diagonal term. *}
    1.19    by best
    1.20  
    1.21 -lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
    1.22 +schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
    1.23    -- {* This form exploits the set constructs. *}
    1.24    by (rule notI, erule rangeE, best)
    1.25  
    1.26 -lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
    1.27 +schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
    1.28    -- {* Or just this! *}
    1.29    by best
    1.30