src/FOLP/ex/Classical.thy

 "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
       (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
   by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 58  NOT PROVED AUTOMATICALLY"
-schematic_lemma
-  notes f_cong = subst_context [where t = f]
-  shows "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
+schematic_lemma "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
+  supply f_cong = subst_context [where t = f]
   by (tactic {* fast_tac @{context} (FOLP_cs addSIs [@{thm f_cong}]) 1 *})
 
 text "Problem 59"
 schematic_lemma "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
   by (tactic "best_tac @{context} FOLP_dup_cs 1")