# HG changeset patch
# User paulson
# Date 963486022 -7200
# Node ID 8adf653d40a1157750fa387b944b253681c3f29f
# Parent  de04717eed7855bf60c47a35f198621bd9253dba
le_refl_iff as default rule

diff -r de04717eed78 -r 8adf653d40a1 src/ZF/Ordinal.ML
--- a/src/ZF/Ordinal.ML	Thu Jul 13 12:59:26 2000 +0200
+++ b/src/ZF/Ordinal.ML	Thu Jul 13 13:00:22 2000 +0200
@@ -267,9 +267,7 @@
 by (asm_simp_tac (simpset() addsimps [lt_not_refl, le_iff]) 1);
 qed "le_refl_iff";
 
-Addsimps [le_refl_iff];
-AddSIs [le_refl];
-AddSDs [le_refl_iff RS iffD1];
+AddIffs [le_refl_iff];
 
 val [prem] = Goal "(~ (i=j & Ord(j)) ==> i<j) ==> i le j";
 by (rtac (disjCI RS (le_iff RS iffD2)) 1);