src/HOL/Tools/specification_package.ML
changeset 19876 11d447d5d68c
parent 19585 70a1ce3b23ae
child 20344 d02b43ea722e
equal deleted inserted replaced
19875:7405ce9d4f25 19876:11d447d5d68c
    81         SOME axname => mk_axiomatic axname cos (apsnd (HOLogic.dest_Trueprop o concl_of) arg)
    81         SOME axname => mk_axiomatic axname cos (apsnd (HOLogic.dest_Trueprop o concl_of) arg)
    82       | NONE => mk_definitional cos arg
    82       | NONE => mk_definitional cos arg
    83 end
    83 end
    84 
    84 
    85 fun add_specification axiomatic cos arg =
    85 fun add_specification axiomatic cos arg =
    86     arg |> apsnd freezeT
    86     arg |> apsnd Thm.freezeT
    87         |> proc_exprop axiomatic cos
    87         |> proc_exprop axiomatic cos
    88         |> apsnd standard
    88         |> apsnd standard
    89 
    89 
    90 fun add_spec x y (context, thm) =
    90 fun add_spec x y (context, thm) =
    91   (Context.the_theory context, thm) |> add_specification x y |>> Context.Theory;
    91   (Context.the_theory context, thm) |> add_specification x y |>> Context.Theory;
   221                 val alt_names = map fst alt_props
   221                 val alt_names = map fst alt_props
   222                 val _ = if exists (fn(name,_) => not (name = "")) alt_names
   222                 val _ = if exists (fn(name,_) => not (name = "")) alt_names
   223                         then writeln "specification"
   223                         then writeln "specification"
   224                         else ()
   224                         else ()
   225             in
   225             in
   226                 arg |> apsnd freezeT
   226                 arg |> apsnd Thm.freezeT
   227                     |> process_all (zip3 alt_names rew_imps frees)
   227                     |> process_all (zip3 alt_names rew_imps frees)
   228             end
   228             end
   229             fun post_proc (context, th) =
   229             fun post_proc (context, th) =
   230                 post_process (Context.theory_of context, th) |>> Context.Theory;
   230                 post_process (Context.theory_of context, th) |>> Context.Theory;
   231     in
   231     in