# HG changeset patch
# User paulson
# Date 905443599 -7200
# Node ID a2109bb8ce2becf45b71ebc525b3966f70177703
# Parent  4abb47b79b86a0d93d00c8cffa243a919121175a
well-formed asym rules; also adds less_irrefl, le_refl since order_refl
and order_less_irrefl are no longer included by AddIffs

diff -r 4abb47b79b86 -r a2109bb8ce2b src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Thu Sep 10 17:50:06 1998 +0200
+++ b/src/HOL/NatDef.ML	Thu Sep 10 18:06:39 1998 +0200
@@ -160,8 +160,8 @@
 by (blast_tac (claset() addIs [wf_pred_nat, wf_trancl RS wf_asym])1);
 qed "less_not_sym";
 
-(* [| n<m; m<n |] ==> R *)
-bind_thm ("less_asym", (less_not_sym RS notE));
+(* [| n<m; ~P ==> m<n |] ==> P *)
+bind_thm ("less_asym", less_not_sym RS swap);
 
 Goalw [less_def] "~ n<(n::nat)";
 by (rtac notI 1);
@@ -170,9 +170,10 @@
 
 (* n<n ==> R *)
 bind_thm ("less_irrefl", (less_not_refl RS notE));
+AddSEs [less_irrefl];
 
 Goal "n<m ==> m ~= (n::nat)";
-by (blast_tac (claset() addSEs [less_irrefl]) 1);
+by (Blast_tac 1);
 qed "less_not_refl2";
 
 (* s < t ==> s ~= t *)
@@ -221,7 +222,7 @@
 Goal "m<n ==> Suc(m) < Suc(n)";
 by (etac rev_mp 1);
 by (nat_ind_tac "n" 1);
-by (ALLGOALS (fast_tac (claset() addEs  [less_trans, lessE])));
+by (ALLGOALS (fast_tac (claset() addEs [less_trans, lessE])));
 qed "Suc_mono";
 
 (*"Less than" is a linear ordering*)
@@ -429,6 +430,7 @@
 Goal "n <= (n::nat)";
 by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
 qed "le_refl";
+AddSIs [le_refl];
 
 (*Obvious ways of proving m<=n; 
   adding these rules to claset might be risky*)