equal
deleted
inserted
replaced
1 signature QUOTIENT = |
1 signature QUOTIENT = |
2 sig |
2 sig |
3 val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
3 val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
4 val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
4 val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
|
5 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
|
6 val note: binding * thm -> local_theory -> thm * local_theory |
5 end; |
7 end; |
6 |
8 |
7 structure Quotient: QUOTIENT = |
9 structure Quotient: QUOTIENT = |
8 struct |
10 struct |
9 |
11 |