equal
deleted
inserted
replaced
9 sig |
9 sig |
10 val quotient_def: (Attrib.binding * mixfix) option * (Attrib.binding * (term * term)) -> |
10 val quotient_def: (Attrib.binding * mixfix) option * (Attrib.binding * (term * term)) -> |
11 local_theory -> (term * thm) * local_theory |
11 local_theory -> (term * thm) * local_theory |
12 |
12 |
13 val quotdef_cmd: (Attrib.binding * mixfix) option * (Attrib.binding * (string * string)) -> |
13 val quotdef_cmd: (Attrib.binding * mixfix) option * (Attrib.binding * (string * string)) -> |
14 local_theory -> local_theory |
14 local_theory -> (term * thm) * local_theory |
15 end; |
15 end; |
16 |
16 |
17 structure Quotient_Def: QUOTIENT_DEF = |
17 structure Quotient_Def: QUOTIENT_DEF = |
18 struct |
18 struct |
19 |
19 |
68 val lhs = Syntax.read_term lthy lhs_str |
68 val lhs = Syntax.read_term lthy lhs_str |
69 val rhs = Syntax.read_term lthy rhs_str |
69 val rhs = Syntax.read_term lthy rhs_str |
70 val lthy' = Variable.declare_term lhs lthy |
70 val lthy' = Variable.declare_term lhs lthy |
71 val lthy'' = Variable.declare_term rhs lthy' |
71 val lthy'' = Variable.declare_term rhs lthy' |
72 in |
72 in |
73 quotient_def (bindmx, (attr, (lhs, rhs))) lthy'' |> snd |
73 quotient_def (bindmx, (attr, (lhs, rhs))) lthy'' |
74 end |
74 end |
75 |
75 |
76 val binding_mixfix_parser = OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where" |
76 val binding_mixfix_parser = OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where" |
77 val quotdef_parser = |
77 val quotdef_parser = |
78 (Scan.option binding_mixfix_parser) -- |
78 (Scan.option binding_mixfix_parser) -- |
79 OuterParse.!!! (SpecParse.opt_thm_name ":" -- ((OuterParse.term --| OuterParse.$$$ "is") -- OuterParse.term)) |
79 OuterParse.!!! (SpecParse.opt_thm_name ":" -- ((OuterParse.term --| OuterParse.$$$ "is") -- OuterParse.term)) |
80 |
80 |
81 val _ = |
81 val _ = |
82 OuterSyntax.local_theory "quotient_definition" |
82 OuterSyntax.local_theory "quotient_definition" |
83 "definition for constants over the quotient type" |
83 "definition for constants over the quotient type" |
84 OuterKeyword.thy_decl (quotdef_parser >> (quotdef_cmd)) |
84 OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd)) |
85 |
85 |
86 end; (* structure *) |
86 end; (* structure *) |