diff -r fa4ebbd350ae -r 4645502c3c64 src/FOLP/ex/If.thy
--- a/src/FOLP/ex/If.thy	Tue Oct 06 13:31:44 2015 +0200
+++ b/src/FOLP/ex/If.thy	Tue Oct 06 15:14:28 2015 +0200
@@ -5,14 +5,14 @@
 definition "if" :: "[o,o,o]=>o" where
   "if(P,Q,R) == P&Q | ~P&R"
 
-schematic_lemma ifI:
+schematic_goal ifI:
   assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
   shows "?p : if(P,Q,R)"
 apply (unfold if_def)
 apply (tactic \<open>fast_tac @{context} (FOLP_cs addIs @{thms assms}) 1\<close>)
 done
 
-schematic_lemma ifE:
+schematic_goal ifE:
   assumes 1: "p : if(P,Q,R)" and
     2: "!!x y. [| x : P; y : Q |] ==> f(x, y) : S" and
     3: "!!x y. [| x : ~P; y : R |] ==> g(x, y) : S"
@@ -22,7 +22,7 @@
 apply (tactic \<open>fast_tac @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1\<close>)
 done
 
-schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
+schematic_goal if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
 apply (rule iffI)
 apply (erule ifE)
 apply (erule ifE)
@@ -32,11 +32,11 @@
 
 ML \<open>val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}]\<close>
 
-schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
+schematic_goal if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
 apply (tactic \<open>fast_tac @{context} if_cs 1\<close>)
 done
 
-schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
+schematic_goal nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
 apply (tactic \<open>fast_tac @{context} if_cs 1\<close>)
 done