--- a/src/Pure/Pure.thy Sun Apr 24 20:37:24 2016 +0200
+++ b/src/Pure/Pure.thy Sun Apr 24 21:31:14 2016 +0200
@@ -54,7 +54,7 @@
and "note" :: prf_decl % "proof"
and "supply" :: prf_script % "proof"
and "using" "unfolding" :: prf_decl % "proof"
- and "fix" "assume" "presume" "def" :: prf_asm % "proof"
+ and "fix" "assume" "presume" "define" "def" :: prf_asm % "proof"
and "consider" :: prf_goal % "proof"
and "obtain" :: prf_asm_goal % "proof"
and "guess" :: prf_script_asm_goal % "proof"
@@ -739,6 +739,11 @@
(structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
val _ =
+ Outer_Syntax.command @{command_keyword define} "local definition (non-polymorphic)"
+ ((Parse.fixes --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
+ >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
+
+val _ =
Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
(Parse.and_list1
(Parse_Spec.opt_thm_name ":" --