equal
deleted
inserted
replaced
22 |
22 |
23 (*code equations and certificates*) |
23 (*code equations and certificates*) |
24 val mk_eqn: theory -> thm * bool -> thm * bool |
24 val mk_eqn: theory -> thm * bool -> thm * bool |
25 val mk_eqn_liberal: theory -> thm -> (thm * bool) option |
25 val mk_eqn_liberal: theory -> thm -> (thm * bool) option |
26 val assert_eqn: theory -> thm * bool -> thm * bool |
26 val assert_eqn: theory -> thm * bool -> thm * bool |
|
27 val assert_abs_eqn: theory -> string option -> thm -> thm * string |
27 val const_typ_eqn: theory -> thm -> string * typ |
28 val const_typ_eqn: theory -> thm -> string * typ |
28 val expand_eta: theory -> int -> thm -> thm |
29 val expand_eta: theory -> int -> thm -> thm |
29 type cert |
30 type cert |
30 val constrain_cert: theory -> sort list -> cert -> cert |
31 val constrain_cert: theory -> sort list -> cert -> cert |
31 val conclude_cert: cert -> cert |
32 val conclude_cert: cert -> cert |