equal
deleted
inserted
replaced
207 (P.opt_locale_target -- Scan.repeat1 constdef |
207 (P.opt_locale_target -- Scan.repeat1 constdef |
208 >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args))); |
208 >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args))); |
209 |
209 |
210 val abbreviationP = |
210 val abbreviationP = |
211 OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl |
211 OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl |
212 (P.opt_locale_target -- |
212 (P.opt_locale_target -- opt_mode -- |
213 Scan.optional (P.$$$ "(" -- P.$$$ "output" -- P.$$$ ")" >> K true) false -- |
|
214 Scan.repeat1 (Scan.option constdecl -- P.prop) |
213 Scan.repeat1 (Scan.option constdecl -- P.prop) |
215 >> (fn ((loc, revert), args) => |
214 >> (fn ((loc, revert), args) => |
216 Toplevel.local_theory loc (Specification.abbreviation revert args))); |
215 Toplevel.local_theory loc (Specification.abbreviation revert args))); |
217 |
216 |
218 |
217 |