# HG changeset patch
# User nipkow
# Date 968239945 -7200
# Node ID c50349d252b7749ef5c079ef9112dd9e6f839595
# Parent  0aa0874ab66bf13a46e3b4a2636fe773ea729b37
imp_cong bound at thm level.

diff -r 0aa0874ab66b -r c50349d252b7 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Sep 06 11:48:51 2000 +0200
+++ b/src/HOL/simpdata.ML	Wed Sep 06 13:32:25 2000 +0200
@@ -70,9 +70,9 @@
    "(? x. x=t & P(x)) = P(t)",          (*essential for termination!!*)
    "(! x. t=x --> P(x)) = P(t)" ];      (*covers a stray case*)
 
-val imp_cong = impI RSN
+val imp_cong = standard(impI RSN
     (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
-        (fn _=> [(Blast_tac 1)]) RS mp RS mp);
+        (fn _=> [(Blast_tac 1)]) RS mp RS mp));
 
 (*Miniscoping: pushing in existential quantifiers*)
 val ex_simps = map prover
@@ -109,6 +109,7 @@
 bind_thms ("ex_simps", ex_simps);
 bind_thms ("all_simps", all_simps);
 bind_thm ("not_not", not_not);
+bind_thm ("imp_cong", imp_cong);
 
 (* Elimination of True from asumptions: *)