# HG changeset patch
# User oheimb
# Date 982249238 -3600
# Node ID 8fd0dea26286eb8872eae54d0c0f5dbf04e67b14
# Parent  8bc06c4202cd6fb6f9308e4ff2b33fdef8819240
moved wf_less from Nat.ML to NatDef.ML

diff -r 8bc06c4202cd -r 8fd0dea26286 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Thu Feb 15 16:00:36 2001 +0100
+++ b/src/HOL/NatDef.ML	Thu Feb 15 16:00:38 2001 +0100
@@ -114,12 +114,17 @@
 
 (*** Basic properties of "less than" ***)
 
-Goalw [wf_def, pred_nat_def] "wf(pred_nat)";
+Goalw [wf_def, pred_nat_def] "wf pred_nat";
 by (Clarify_tac 1);
 by (nat_ind_tac "x" 1);
 by (ALLGOALS Blast_tac);
 qed "wf_pred_nat";
 
+Goalw [less_def] "wf {(x,y::nat). x<y}"; 
+by (rtac (wf_pred_nat RS wf_trancl RS wf_subset) 1);
+by (Blast_tac 1); 
+qed "wf_less";
+
 (*Used in TFL/post.sml*)
 Goalw [less_def] "(m,n) : pred_nat^+ = (m<n)";
 by (rtac refl 1);