--- a/src/Pure/Pure.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/Pure/Pure.thy Sun Dec 03 13:22:09 2017 +0100
@@ -55,7 +55,7 @@
and "note" :: prf_decl % "proof"
and "supply" :: prf_script % "proof"
and "using" "unfolding" :: prf_decl % "proof"
- and "fix" "assume" "presume" "define" "def" :: prf_asm % "proof"
+ and "fix" "assume" "presume" "define" :: prf_asm % "proof"
and "consider" :: prf_goal % "proof"
and "obtain" :: prf_asm_goal % "proof"
and "guess" :: prf_script_asm_goal % "proof"
@@ -807,15 +807,6 @@
>> (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 ":" --
- ((Parse.binding -- Parse.opt_mixfix) --
- ((@{keyword \<equiv>} || @{keyword ==}) |-- Parse.!!! Parse.termp)))
- >> (fn args => Toplevel.proof (fn state =>
- (legacy_feature "Old 'def' command -- use 'define' instead"; Proof.def_cmd args state))));
-
-val _ =
Outer_Syntax.command @{command_keyword consider} "state cases rule"
(Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));