equal
deleted
inserted
replaced
32 val eqvt_raw_del: attribute |
32 val eqvt_raw_del: attribute |
33 val setup: theory -> theory |
33 val setup: theory -> theory |
34 val get_eqvts_thms: Proof.context -> thm list |
34 val get_eqvts_thms: Proof.context -> thm list |
35 val get_eqvts_raw_thms: Proof.context -> thm list |
35 val get_eqvts_raw_thms: Proof.context -> thm list |
36 |
36 |
|
37 (* TEMPORARY FIX *) |
|
38 val add_thm: thm -> Context.generic -> Context.generic |
|
39 val add_raw_thm: thm -> Context.generic -> Context.generic |
37 end; |
40 end; |
38 |
41 |
39 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
42 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
40 struct |
43 struct |
41 |
44 |