equal
deleted
inserted
replaced
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 val eqvt_transform: Proof.context -> thm -> thm |
36 val eqvt_transform: Proof.context -> thm -> thm |
37 val is_eqvt: Proof.context -> term -> bool |
37 val is_eqvt: Proof.context -> term -> bool |
38 |
|
39 (* TEMPORARY FIX *) |
|
40 val add_thm: thm -> Context.generic -> Context.generic |
|
41 val add_raw_thm: thm -> Context.generic -> Context.generic |
|
42 end; |
38 end; |
43 |
39 |
44 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
40 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
45 struct |
41 struct |
46 |
42 |