# HG changeset patch # User paulson # Date 859973267 -7200 # Node ID 7d640451ae7d0b1719f744bd1cacfb53c656165d # Parent 1f3f5c44e159925da4716d7ba897659a70ebfb23 Now tests for essential ancestors (Lfp or Gfp) diff -r 1f3f5c44e159 -r 7d640451ae7d src/HOL/add_ind_def.ML --- a/src/HOL/add_ind_def.ML Wed Apr 02 11:25:04 1997 +0200 +++ b/src/HOL/add_ind_def.ML Wed Apr 02 11:27:47 1997 +0200 @@ -31,9 +31,10 @@ signature FP = (** Description of a fixed point operator **) sig + val checkThy : theory -> unit (*signals error if Lfp/Gfp is missing*) val oper : string * typ * term -> term (*fixed point operator*) - val Tarski : thm (*Tarski's fixed point theorem*) - val induct : thm (*induction/coinduction rule*) + val Tarski : thm (*Tarski's fixed point theorem*) + val induct : thm (*induction/coinduction rule*) end; @@ -52,6 +53,8 @@ (*internal version*) fun add_fp_def_i (rec_tms, intr_tms) thy = let + val dummy = Fp.checkThy thy (*has essential ancestors?*) + val sign = sign_of thy; (*rec_params should agree for all mutually recursive components*)