Now calls require_thy to ensure ancestors are present
authorpaulson
Wed Apr 02 11:16:40 1997 +0200 (1997-04-02)
changeset 285536f75c4a0047
parent 2854 f03b1652fc6a
child 2856 cdb908486a96
Now calls require_thy to ensure ancestors are present
src/HOL/Inductive.ML
     1.1 --- a/src/HOL/Inductive.ML	Wed Apr 02 11:15:46 1997 +0200
     1.2 +++ b/src/HOL/Inductive.ML	Wed Apr 02 11:16:40 1997 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4  
     1.5  structure Lfp_items =
     1.6    struct
     1.7 +  val checkThy	= (fn thy => require_thy thy "Lfp" "inductive definitions")
     1.8    val oper      = gen_fp_oper "lfp"
     1.9    val Tarski    = def_lfp_Tarski
    1.10    val induct    = def_induct
    1.11 @@ -25,6 +26,7 @@
    1.12  
    1.13  structure Gfp_items =
    1.14    struct
    1.15 +  val checkThy	= (fn thy => require_thy thy "Gfp" "coinductive definitions")
    1.16    val oper      = gen_fp_oper "gfp"
    1.17    val Tarski    = def_gfp_Tarski
    1.18    val induct    = def_Collect_coinduct
    1.19 @@ -63,7 +65,7 @@
    1.20    end;
    1.21  
    1.22  
    1.23 -(*For upwards compatibility: can be called directly from ML*)
    1.24 +(*Called by the theory sections or directly from ML*)
    1.25  functor Inductive_Fun
    1.26   (Inductive: sig include INDUCTIVE_STRING INDUCTIVE_ARG end)
    1.27     : sig include INTR_ELIM INDRULE end =