src/HOL/simpdata.ML
changeset 9875 c50349d252b7
parent 9851 e22db9397e17
child 9876 a069795f1060
     1.1 --- a/src/HOL/simpdata.ML	Wed Sep 06 11:48:51 2000 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Wed Sep 06 13:32:25 2000 +0200
     1.3 @@ -70,9 +70,9 @@
     1.4     "(? x. x=t & P(x)) = P(t)",          (*essential for termination!!*)
     1.5     "(! x. t=x --> P(x)) = P(t)" ];      (*covers a stray case*)
     1.6  
     1.7 -val imp_cong = impI RSN
     1.8 +val imp_cong = standard(impI RSN
     1.9      (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
    1.10 -        (fn _=> [(Blast_tac 1)]) RS mp RS mp);
    1.11 +        (fn _=> [(Blast_tac 1)]) RS mp RS mp));
    1.12  
    1.13  (*Miniscoping: pushing in existential quantifiers*)
    1.14  val ex_simps = map prover
    1.15 @@ -109,6 +109,7 @@
    1.16  bind_thms ("ex_simps", ex_simps);
    1.17  bind_thms ("all_simps", all_simps);
    1.18  bind_thm ("not_not", not_not);
    1.19 +bind_thm ("imp_cong", imp_cong);
    1.20  
    1.21  (* Elimination of True from asumptions: *)
    1.22