56   val transform_prem1: Proof.context -> string list -> thm -> thm

    56   val transform_prem1: Proof.context -> string list -> thm -> thm

    57   val transform_prem2: Proof.context -> string list -> thm -> thm

    57   val transform_prem2: Proof.context -> string list -> thm -> thm

    58 

    58 

    59   (* transformation into the object logic *)

    59   (* transformation into the object logic *)

    60   val atomize: thm -> thm

    60   val atomize: thm -> thm

    61 end

    62 end

    62 

    63 

    63 

    64 

    64 structure Nominal_Library: NOMINAL_LIBRARY =

    65 structure Nominal_Library: NOMINAL_LIBRARY =

    65 struct

    66 struct

   260 

   261 

   261 

   262 

   262 (* transformes a theorem into one of the object logic *)

   263 (* transformes a theorem into one of the object logic *)

   263 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars

   264 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars

   264 

   265 

   266 end (* structure *)

   266 end (* structure *)

   267 

   267 

   268 open Nominal_Library;

   268 open Nominal_Library;