# HG changeset patch
# User paulson
# Date 962181606 -7200
# Node ID 7a98dbf3e5796644aa68cb0c304db12bc3ae4120
# Parent  902ea754eee21a90cfdb9f970b451a6269d96110
using the new theorem wf_not_refl; tidied

diff -r 902ea754eee2 -r 7a98dbf3e579 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Wed Jun 28 10:39:02 2000 +0200
+++ b/src/HOL/NatDef.ML	Wed Jun 28 10:40:06 2000 +0200
@@ -159,12 +159,11 @@
 bind_thm ("less_asym", less_not_sym RS swap);
 
 Goalw [less_def] "~ n<(n::nat)";
-by (rtac notI 1);
-by (etac (wf_pred_nat RS wf_trancl RS wf_irrefl) 1);
+by (rtac (wf_pred_nat RS wf_trancl RS wf_not_refl) 1);
 qed "less_not_refl";
 
 (* n<n ==> R *)
-bind_thm ("less_irrefl", (less_not_refl RS notE));
+bind_thm ("less_irrefl", less_not_refl RS notE);
 AddSEs [less_irrefl];
 
 Goal "n<m ==> m ~= (n::nat)";
@@ -293,7 +292,7 @@
 
 (*Complete induction, aka course-of-values induction*)
 val prems = Goalw [less_def]
-    "[| !!n. [| ! m::nat. m<n --> P(m) |] ==> P(n) |]  ==>  P(n)";
+    "[| !!n. [| ALL m::nat. m<n --> P(m) |] ==> P(n) |]  ==>  P(n)";
 by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1);
 by (eresolve_tac prems 1);
 qed "less_induct";
@@ -465,7 +464,7 @@
 
 (** LEAST -- the least number operator **)
 
-Goal "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)";
+Goal "(ALL m::nat. P m --> n <= m) = (ALL m. m < n --> ~ P m)";
 by (blast_tac (claset() addIs [leI] addEs [leE]) 1);
 val lemma = result();
 
@@ -514,7 +513,7 @@
 (* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *)
 bind_thm("nat_neqE", nat_neq_iff RS iffD1 RS disjE);
 
-Goal "(S::nat set) ~= {} ==> ? x:S. ! y:S. x <= y";
+Goal "(S::nat set) ~= {} ==> EX x:S. ALL y:S. x <= y";
 by (cut_facts_tac [wf_pred_nat RS wf_trancl RS (wf_eq_minimal RS iffD1)] 1);
 by (dres_inst_tac [("x","S")] spec 1);
 by (Asm_full_simp_tac 1);