Nat.ML

 
 val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = n::nat";
 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];