# HG changeset patch
# User oheimb
# Date 949064963 -3600
# Node ID b4700243eb9cfc975a59d4d4a5cd6e545379d8c7
# Parent  b1a458416c929d804d1c0f469e49e819ab4af096
added full_nat_induct

diff -r b1a458416c92 -r b4700243eb9c src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Fri Jan 28 14:08:54 2000 +0100
+++ b/src/HOL/WF_Rel.ML	Fri Jan 28 14:09:23 2000 +0100
@@ -26,6 +26,12 @@
 qed "less_than_iff";
 AddIffs [less_than_iff];
 
+Goal "(!!n. (!m. Suc m <= n --> P m) ==> P n) ==> P n";
+br (wf_less_than RS wf_induct) 1;
+by (resolve_tac (premises()) 1);
+by Auto_tac;
+qed_spec_mp "full_nat_induct";
+
 (*----------------------------------------------------------------------------
  * The inverse image into a wellfounded relation is wellfounded.
  *---------------------------------------------------------------------------*)