# HG changeset patch
# User wenzelm
# Date 1213200096 -7200
# Node ID 192954a9a549d00bdfd47d9d91e742e81cfd3562
# Parent  bd387c1a05368d934fd2d1b944ede9ca9fffb611
changed pred_congs: merely cover pred1_cong pred2_cong pred3_cong;

diff -r bd387c1a0536 -r 192954a9a549 src/FOLP/IFOLP.thy
--- 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]