src/HOL/Tools/inductive_package.ML
changeset 17010 5abc26872268
parent 16975 34ed8d5d4f16
child 17057 0934ac31985f
equal deleted inserted replaced
17009:932e0e370926 17010:5abc26872268
    63 
    63 
    64 
    64 
    65 (** theory context references **)
    65 (** theory context references **)
    66 
    66 
    67 val mono_name = "Orderings.mono";
    67 val mono_name = "Orderings.mono";
    68 val gfp_name = "Gfp.gfp";
    68 val gfp_name = "FixedPoint.gfp";
    69 val lfp_name = "Lfp.lfp";
    69 val lfp_name = "FixedPoint.lfp";
    70 val vimage_name = "Set.vimage";
    70 val vimage_name = "Set.vimage";
    71 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
    71 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
    72 
    72 
    73 val inductive_forall_name = "HOL.induct_forall";
    73 val inductive_forall_name = "HOL.induct_forall";
    74 val inductive_forall_def = thm "induct_forall_def";
    74 val inductive_forall_def = thm "induct_forall_def";