On 31/08/16 11:04, Burkhart Wolff wrote:
>
> fun check_hyps context th =
> (case undeclared_hyps context th of
> [] => th
> | undeclared =>
> error (Pretty.string_of (Pretty.big_list "Undeclared hyps:"
> (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty
>
Dear all,
in the past, we used the kernel operation Thm.assume to generate and manage
proof-obligations.
This had the advantage that they can be displayed and handled transparently;
and then eventually
discharged by later processes.
Apparently, having thm's in the theory context is no longer
