--- a/src/FOLP/IFOLP.thy Wed Jun 11 18:01:11 2008 +0200
+++ b/src/FOLP/IFOLP.thy Wed Jun 11 18:01:36 2008 +0200
@@ -500,15 +500,7 @@
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
done
-(*special cases for free variables P, Q, R, S -- up to 3 arguments*)
-
-ML {*
- bind_thms ("pred_congs",
- flat (map (fn c =>
- map (fn th => read_instantiate [("P",c)] th)
- [@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}])
- (explode"PQRS")))
-*}
+lemmas pred_congs = pred1_cong pred2_cong pred3_cong
(*special case for the equality predicate!*)
lemmas eq_cong = pred2_cong [where P = "op =", standard]