src/HOL/Tools/inductive_package.ML
changeset 11755 d12864826f4c
parent 11740 86ac4189a1c1
child 11770 b6bb7a853dd2
equal deleted inserted replaced
11754:3928d990c22f 11755:d12864826f4c
    65 struct
    65 struct
    66 
    66 
    67 
    67 
    68 (** theory context references **)
    68 (** theory context references **)
    69 
    69 
    70 val mono_name = "Ord.mono";
    70 val mono_name = "HOL.mono";
    71 val gfp_name = "Gfp.gfp";
    71 val gfp_name = "Gfp.gfp";
    72 val lfp_name = "Lfp.lfp";
    72 val lfp_name = "Lfp.lfp";
    73 val vimage_name = "Inverse_Image.vimage";
    73 val vimage_name = "Inverse_Image.vimage";
    74 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
    74 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
    75 
    75