HOL/Nat/less_asym: renamed from less_anti_sym

--- a/Nat.ML	Fri Jun 24 15:10:13 1994 +0200
+++ b/Nat.ML	Fri Jun 24 15:11:39 1994 +0200
@@ -219,11 +219,11 @@
 (** Elimination properties **)
 
 val prems = goalw Nat.thy [less_def] "n<m ==> ~ m<n::nat";
-by(fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_anti_sym]@prems))1);
+by(fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
 val less_not_sym = result();
 
 (* [| n<m; m<n |] ==> R *)
-val less_anti_sym = standard (less_not_sym RS notE);
+val less_asym = standard (less_not_sym RS notE);
 
 goalw Nat.thy [less_def] "~ n<n::nat";
 by (rtac notI 1);
@@ -380,7 +380,7 @@
 
 goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
 by(simp_tac nat_ss 1);
-by (fast_tac (HOL_cs addEs [less_anti_refl,less_anti_sym]) 1);
+by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
 val lessD = result();
 
 goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
@@ -389,17 +389,17 @@
 val Suc_leD = result();
 
 goalw Nat.thy [le_def] "!!m. m < n ==> m <= n::nat";
-by (fast_tac (HOL_cs addEs [less_anti_sym]) 1);
+by (fast_tac (HOL_cs addEs [less_asym]) 1);
 val less_imp_le = result();
 
 goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=n::nat";
 by (cut_facts_tac [less_linear] 1);
-by (fast_tac (HOL_cs addEs [less_anti_refl,less_anti_sym]) 1);
+by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
 val le_imp_less_or_eq = result();
 
 goalw Nat.thy [le_def] "!!m. m<n | m=n ==> m <= n::nat";
 by (cut_facts_tac [less_linear] 1);
-by (fast_tac (HOL_cs addEs [less_anti_refl,less_anti_sym]) 1);
+by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
 by (flexflex_tac);
 val less_or_eq_imp_le = result();
 
@@ -423,7 +423,7 @@
 
 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])]);
+          fast_tac (HOL_cs addEs [less_anti_refl,less_asym])]);
 val le_anti_sym = result();
 
 val nat_ss = nat_ss addsimps [le_refl];