equal
deleted
inserted
replaced
5 Definitions and proofs for the alpha-relations. |
5 Definitions and proofs for the alpha-relations. |
6 *) |
6 *) |
7 |
7 |
8 signature NOMINAL_DT_ALPHA = |
8 signature NOMINAL_DT_ALPHA = |
9 sig |
9 sig |
10 val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> |
10 val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> |
11 term list -> Proof.context -> term list * term list * thm list * thm list * thm * local_theory |
11 bclause list list list -> term list -> Proof.context -> |
|
12 term list * term list * thm list * thm list * thm * local_theory |
12 |
13 |
13 val mk_alpha_distincts: Proof.context -> thm list -> thm list -> |
14 val mk_alpha_distincts: Proof.context -> thm list -> thm list -> |
14 term list -> typ list -> thm list |
15 term list -> typ list -> thm list |
15 |
16 |
16 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
17 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |