Removal of COND_CONG, which is just if_cong RS eq_reflection
authorpaulson
Mon Jun 23 11:30:35 1997 +0200 (1997-06-23)
changeset 34585ff4bfab859c
parent 3457 a8ab7c64817c
child 3459 112cbb8301dc
Removal of COND_CONG, which is just if_cong RS eq_reflection
TFL/thms.sig
TFL/thms.sml
     1.1 --- a/TFL/thms.sig	Mon Jun 23 10:42:03 1997 +0200
     1.2 +++ b/TFL/thms.sig	Mon Jun 23 11:30:35 1997 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4     val CUT_LEMMA       :thm
     1.5     val SELECT_AX       :thm
     1.6     
     1.7 -   val COND_CONG :thm
     1.8     val LET_CONG  :thm
     1.9  
    1.10     val eqT       :thm
     2.1 --- a/TFL/thms.sml	Mon Jun 23 10:42:03 1997 +0200
     2.2 +++ b/TFL/thms.sml	Mon Jun 23 11:30:35 1997 +0200
     2.3 @@ -19,7 +19,7 @@
     2.4     end;
     2.5  
     2.6    (*-------------------------------------------------------------------------
     2.7 -   *  A useful congruence rule
     2.8 +   *  Congruence rule needed for TFL, but not for general simplification
     2.9     *-------------------------------------------------------------------------*)
    2.10     local val [p1,p2] = goal HOL.thy "(M = N) ==> \
    2.11                            \ (!!x. ((x = N) ==> (f x = g x))) ==> \
    2.12 @@ -27,10 +27,7 @@
    2.13           val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
    2.14           val _ = by (rtac p2 1);
    2.15           val _ = by (rtac refl 1);
    2.16 -   in val LET_CONG = result() RS eq_reflection
    2.17 -   end;
    2.18 -
    2.19 -   val COND_CONG = if_cong RS eq_reflection;
    2.20 +   in val LET_CONG = result() end;
    2.21  
    2.22     fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
    2.23