diff -r bc6e2936a293 -r ac6cf9f18653 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Fri Feb 20 17:33:14 1998 +0100
+++ b/src/HOL/NatDef.ML	Fri Feb 20 17:56:39 1998 +0100
@@ -588,7 +588,15 @@
 by (blast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
 qed "nat_less_le";
 
-(** max **)
+(* Axiom 'linorder_linear' of class 'linorder': *)
+goal thy "(m::nat) <= n | n <= m";
+by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
+by (cut_facts_tac [less_linear] 1);
+by(Blast_tac 1);
+qed "nat_le_linear";
+
+
+(** max
 
 goalw thy [max_def] "!!z::nat. (z <= max x y) = (z <= x | z <= y)";
 by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
@@ -612,7 +620,7 @@
 by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
 by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
 qed "min_le_iff_disj";
-
+ **)
 
 (** LEAST -- the least number operator **)
 
@@ -624,8 +632,6 @@
 goalw thy [Least_def]
   "(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))";
 by (simp_tac (simpset() addsimps [lemma]) 1);
-by (rtac eq_reflection 1);
-by (rtac refl 1);
 qed "Least_nat_def";
 
 val [prem1,prem2] = goalw thy [Least_nat_def]