(* -*- Emacs Mode: sml -*- *)

(*---------------------------------------------------------------------------*)
(*
   File:         mk_gen_induct.sml

   Description:  This file proves the theorem of general induction on natural
                 numbers by using the theorem of primitive recursion.

   Author:       (c) Copyright 1990-2008 by Flemming Andersen
                 Modified by John Harrison to just pick up num_WF instead
   Date:         June 7. 1990
   Last Update:  January 18, 2008
*)
(*---------------------------------------------------------------------------*)

(*
        !P. (!(m:num). (!n. n < m ==> (P n)) ==> (P m)) ==> (!m. P m)
*)
let GEN_INDUCT_thm = prove_thm
  ("GEN_INDUCT_thm",
   (`!P. (!(m:num). (!n. n < m ==> (P n)) ==> (P m)) ==> (!m. P m)`),
    MATCH_ACCEPT_TAC num_WF);;
(* Emacs editor information
|  Local variables:
|  mode:sml
|  sml-prog-name:"hol90"
|  End:
*)