# HG changeset patch
# User paulson
# Date 840618004 -7200
# Node ID c77409a88b75b697f86eb75467c9c7a62cd61e8b
# Parent  cdf9bcd53749584da8806a19579ff07b95f7a172
Added le_eq_less_Suc; fixed some comments;
a bit of tidying up

diff -r cdf9bcd53749 -r c77409a88b75 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Tue Aug 20 18:53:17 1996 +0200
+++ b/src/HOL/Nat.ML	Wed Aug 21 11:00:04 1996 +0200
@@ -234,7 +234,7 @@
 by (fast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
 qed "less_not_sym";
 
-(* [| n(m; m(n |] ==> R *)
+(* [| n<m; m<n |] ==> R *)
 bind_thm ("less_asym", (less_not_sym RS notE));
 
 goalw Nat.thy [less_def] "~ n<(n::nat)";
@@ -392,6 +392,10 @@
 
 (*** Properties of <= ***)
 
+goalw Nat.thy [le_def] "(m <= n) = (m < Suc n)";
+by (rtac not_less_eq 1);
+qed "le_eq_less_Suc";
+
 goalw Nat.thy [le_def] "0 <= n";
 by (rtac not_less0 1);
 qed "le0";
@@ -565,15 +569,14 @@
 qed "not_less_Least";
 
 qed_goalw "Least_Suc" Nat.thy [Least_def]
- "[| ? n. P (Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P (Suc m))"
- (fn prems => [
-	cut_facts_tac prems 1,
+ "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
+ (fn _ => [
 	rtac select_equality 1,
 	fold_goals_tac [Least_def],
 	safe_tac (!claset addSEs [LeastI]),
 	res_inst_tac [("n","j")] natE 1,
 	Fast_tac 1,
-	fast_tac (!claset addDs [Suc_less_SucD] addDs [not_less_Least]) 1,	
+	fast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1,
 	res_inst_tac [("n","k")] natE 1,
 	Fast_tac 1,
 	hyp_subst_tac 1,