--- a/src/HOL/ex/Set_Theory.thy Tue Oct 06 13:31:44 2015 +0200
+++ b/src/HOL/ex/Set_Theory.thy Tue Oct 06 15:14:28 2015 +0200
@@ -27,7 +27,7 @@
Trivial example of term synthesis: apparently hard for some provers!
*}
-schematic_lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
+schematic_goal "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
by blast
@@ -61,15 +61,15 @@
-- {* Requires best-first search because it is undirectional. *}
by best
-schematic_lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
+schematic_goal "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
-- {*This form displays the diagonal term. *}
by best
-schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
+schematic_goal "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
-- {* This form exploits the set constructs. *}
by (rule notI, erule rangeE, best)
-schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
+schematic_goal "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
-- {* Or just this! *}
by best