diff -r 385d51d74f71 -r 194d088c1511 nat.ML
--- a/nat.ML	Tue Mar 22 08:28:31 1994 +0100
+++ b/nat.ML	Tue Mar 22 08:31:58 1994 +0100
@@ -425,3 +425,5 @@
 by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
           fast_tac (HOL_cs addEs [less_anti_refl,less_anti_sym])]);
 val le_anti_sym = result();
+
+val nat_ss = nat_ss addsimps [le_refl];