equal
deleted
inserted
replaced
1 signature QUOTIENT = |
1 signature QUOTIENT = |
2 sig |
2 sig |
3 exception LIFT_MATCH of string |
|
4 |
|
5 val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
3 val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
6 val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
4 val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
7 |
5 |
8 val note: binding * thm -> local_theory -> thm * local_theory |
6 val note: binding * thm -> local_theory -> thm * local_theory |
9 end; |
7 end; |
10 |
8 |
11 structure Quotient: QUOTIENT = |
9 structure Quotient: QUOTIENT = |
12 struct |
10 struct |
13 |
|
14 (* exception for when quotient and lifted things do not match *) |
|
15 exception LIFT_MATCH of string |
|
16 |
11 |
17 (* wrappers for define, note and theorem_i *) |
12 (* wrappers for define, note and theorem_i *) |
18 fun define (name, mx, rhs) lthy = |
13 fun define (name, mx, rhs) lthy = |
19 let |
14 let |
20 val ((rhs, (_ , thm)), lthy') = |
15 val ((rhs, (_ , thm)), lthy') = |