Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CCL/ccl.ML/po_refl_iff_T: deleted reference to make_iff_T
authorlcp
Thu, 17 Mar 1994 12:56:44 +0100
changeset 280 fb379160f4de
parent 279 7738aed3f84d
child 281 f1f96b9e6285
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
src/CCL/CCL.ML file | annotate | diff | comparison | revisions
src/CCL/ccl.ML file | annotate | diff | comparison | revisions 
--- 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 ***)
 
--- 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 ***)
isabelle