equal
deleted
inserted
replaced
145 val prop = Syntax.read_prop lthy propstr |
145 val prop = Syntax.read_prop lthy propstr |
146 in |
146 in |
147 quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd |
147 quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd |
148 end |
148 end |
149 |
149 |
150 |
|
151 val quotdef_parser = |
150 val quotdef_parser = |
152 (OuterParse.binding -- |
151 (OuterParse.binding -- |
153 (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ -- |
152 (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ -- |
154 OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- |
153 OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- |
155 (SpecParse.opt_thm_name ":" -- OuterParse.prop) |
154 (SpecParse.opt_thm_name ":" -- OuterParse.prop) |