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 const_typ_eqn: theory -> thm -> string * typ |
27 val const_typ_eqn: theory -> thm -> string * typ |
28 val expand_eta: theory -> int -> thm -> thm |
28 val expand_eta: theory -> int -> thm -> thm |
29 type cert |
29 type cert |
30 val empty_cert: theory -> string -> cert |
|
31 val cert_of_eqns: theory -> string -> (thm * bool) list -> cert |
|
32 val constrain_cert: theory -> sort list -> cert -> cert |
30 val constrain_cert: theory -> sort list -> cert -> cert |
33 val conclude_cert: cert -> cert |
31 val conclude_cert: cert -> cert |
34 val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list |
32 val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list |
35 val equations_of_cert: theory -> cert -> ((string * sort) list * typ) |
33 val equations_of_cert: theory -> cert -> ((string * sort) list * typ) |
36 * (((term * string option) list * (term * string option)) * (thm option * bool)) list |
34 * (((term * string option) list * (term * string option)) * (thm option * bool)) list |
37 val bare_thms_of_cert: theory -> cert -> thm list |
|
38 val pretty_cert: theory -> cert -> Pretty.T list |
35 val pretty_cert: theory -> cert -> Pretty.T list |
39 |
36 |
40 (*executable code*) |
37 (*executable code*) |
41 val add_datatype: (string * typ) list -> theory -> theory |
38 val add_datatype: (string * typ) list -> theory -> theory |
42 val add_datatype_cmd: string list -> theory -> theory |
39 val add_datatype_cmd: string list -> theory -> theory |
861 o snd o equations_of_cert thy) cert |
858 o snd o equations_of_cert thy) cert |
862 | pretty_cert thy (Projection (t, _)) = |
859 | pretty_cert thy (Projection (t, _)) = |
863 [Syntax.pretty_term_global thy (Logic.varify_types_global t)] |
860 [Syntax.pretty_term_global thy (Logic.varify_types_global t)] |
864 | pretty_cert thy (Abstract (abs_thm, _)) = |
861 | pretty_cert thy (Abstract (abs_thm, _)) = |
865 [(Display.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm]; |
862 [(Display.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm]; |
866 |
|
867 fun bare_thms_of_cert thy (cert as Equations _) = |
|
868 (map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) |
|
869 o snd o equations_of_cert thy) cert |
|
870 | bare_thms_of_cert thy (Projection _) = [] |
|
871 | bare_thms_of_cert thy (Abstract (abs_thm, tyco)) = |
|
872 [Thm.varifyT_global (snd (concretify_abs thy tyco abs_thm))]; |
|
873 |
863 |
874 end; |
864 end; |
875 |
865 |
876 |
866 |
877 (* code certificate access *) |
867 (* code certificate access *) |