--- a/src/Pure/Pure.thy Sat May 28 23:55:41 2016 +0200
+++ b/src/Pure/Pure.thy Sun May 29 15:40:25 2016 +0200
@@ -343,13 +343,14 @@
val _ =
Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
- (Scan.option Parse_Spec.constdecl -- Parse_Spec.spec
- >> (fn (a, (b, c)) => #2 oo Specification.definition_cmd a b c));
+ (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
+ Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) =>
+ #2 oo Specification.definition_cmd decl params prems spec));
val _ =
Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
- (Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
- >> (fn (mode, (a, b)) => Specification.abbreviation_cmd mode a b));
+ (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes
+ >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec));
val axiomatization =
Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) --