# HG changeset patch
# User lcp
# Date 763905404 -3600
# Node ID fb379160f4deed4625cb564cceafbcf364e211a6
# Parent  7738aed3f84dba0f393d0193d66f71ee9e544800
CCL/ccl.ML/po_refl_iff_T: deleted reference to make_iff_T
CCL/ccl.ML/CCL_ss: now includes po_refl RS P_iff_T

diff -r 7738aed3f84d -r fb379160f4de src/CCL/CCL.ML
--- a/src/CCL/CCL.ML	Thu Mar 17 12:36:58 1994 +0100
+++ b/src/CCL/CCL.ML	Thu Mar 17 12:56:44 1994 +0100
@@ -10,10 +10,8 @@
 
 val ccl_data_defs = [apply_def,fix_def];
 
-val po_refl_iff_T = make_iff_T po_refl;
-
 val CCL_ss = FOL_ss addcongs set_congs
-                    addsimps  ([po_refl_iff_T] @ mem_rews);
+                    addsimps  ([po_refl RS P_iff_T] @ mem_rews);
 
 (*** Congruence Rules ***)
 
diff -r 7738aed3f84d -r fb379160f4de src/CCL/ccl.ML
--- a/src/CCL/ccl.ML	Thu Mar 17 12:36:58 1994 +0100
+++ b/src/CCL/ccl.ML	Thu Mar 17 12:56:44 1994 +0100
@@ -10,10 +10,8 @@
 
 val ccl_data_defs = [apply_def,fix_def];
 
-val po_refl_iff_T = make_iff_T po_refl;
-
 val CCL_ss = FOL_ss addcongs set_congs
-                    addsimps  ([po_refl_iff_T] @ mem_rews);
+                    addsimps  ([po_refl RS P_iff_T] @ mem_rews);
 
 (*** Congruence Rules ***)