equal
deleted
inserted
replaced
1 signature QUOTIENT = |
1 signature QUOTIENT = |
2 sig |
2 sig |
3 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 |
4 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 |
5 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
5 |
6 val note: binding * thm -> local_theory -> thm * local_theory |
6 val note: binding * thm -> local_theory -> thm * local_theory |
7 end; |
7 end; |
8 |
8 |
9 structure Quotient: QUOTIENT = |
9 structure Quotient: QUOTIENT = |
10 struct |
10 struct |
210 fun quotient_type_cmd spec lthy = |
210 fun quotient_type_cmd spec lthy = |
211 let |
211 let |
212 fun parse_spec (((qty_str, mx), rty_str), rel_str) = |
212 fun parse_spec (((qty_str, mx), rty_str), rel_str) = |
213 let |
213 let |
214 val qty_name = Binding.name qty_str |
214 val qty_name = Binding.name qty_str |
215 val rty = Syntax.parse_typ lthy rty_str |> Syntax.check_typ lthy |
215 val rty = Syntax.read_typ lthy rty_str |
216 val rel = Syntax.parse_term lthy rel_str |> Syntax.check_term lthy |
216 val rel = Syntax.read_term lthy rel_str |
217 in |
217 in |
218 ((qty_name, mx), (rty, rel)) |
218 ((qty_name, mx), (rty, rel)) |
219 end |
219 end |
220 in |
220 in |
221 quotient_type (map parse_spec spec) lthy |
221 quotient_type (map parse_spec spec) lthy |