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