src/CCL/ccl.ML
changeset 280 fb379160f4de
parent 8 c3d2c6dcf3f0
     1.1 --- a/src/CCL/ccl.ML	Thu Mar 17 12:36:58 1994 +0100
     1.2 +++ b/src/CCL/ccl.ML	Thu Mar 17 12:56:44 1994 +0100
     1.3 @@ -10,10 +10,8 @@
     1.4  
     1.5  val ccl_data_defs = [apply_def,fix_def];
     1.6  
     1.7 -val po_refl_iff_T = make_iff_T po_refl;
     1.8 -
     1.9  val CCL_ss = FOL_ss addcongs set_congs
    1.10 -                    addsimps  ([po_refl_iff_T] @ mem_rews);
    1.11 +                    addsimps  ([po_refl RS P_iff_T] @ mem_rews);
    1.12  
    1.13  (*** Congruence Rules ***)
    1.14