equal
deleted
inserted
replaced
69 ((trm, thm), lthy'') |
69 ((trm, thm), lthy'') |
70 end |
70 end |
71 |
71 |
72 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy = |
72 fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy = |
73 let |
73 let |
74 val lhs = Syntax.read_term lthy lhs_str |
74 val [lhs, rhs] = Syntax.read_terms lthy [lhs_str, rhs_str] |
75 val rhs = Syntax.read_term lthy rhs_str |
|
76 val lthy' = Variable.declare_term lhs lthy |
75 val lthy' = Variable.declare_term lhs lthy |
77 val lthy'' = Variable.declare_term rhs lthy' |
76 val lthy'' = Variable.declare_term rhs lthy' |
78 in |
77 in |
79 quotient_def mx attr lhs rhs lthy'' |> snd |
78 quotient_def mx attr lhs rhs lthy'' |> snd |
80 end |
79 end |
81 |
80 |
82 val _ = OuterKeyword.keyword "as"; |
|
83 |
|
84 val quotdef_parser = |
81 val quotdef_parser = |
85 (SpecParse.opt_thm_name ":" -- |
82 (SpecParse.opt_thm_name ":" -- |
86 OuterParse.term) -- |
83 OuterParse.term) -- |
87 (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" -- |
84 (OuterParse.opt_mixfix' --| OuterParse.$$$ "is" -- |
88 OuterParse.term) |
85 OuterParse.term) |
89 |
86 |
90 val _ = OuterSyntax.local_theory "quotient_definition" |
87 val _ = OuterSyntax.local_theory "quotient_definition" |
91 "definition for constants over the quotient type" |
88 "definition for constants over the quotient type" |
92 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |
89 OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd) |