src/Pure/Pure.thy
changeset 67119 acb0807ddb56
parent 67105 05ff3e6dbbce
child 67147 dea94b1aabc3
     1.1 --- a/src/Pure/Pure.thy	Sat Dec 02 16:50:53 2017 +0000
     1.2 +++ b/src/Pure/Pure.thy	Sun Dec 03 13:22:09 2017 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4    and "note" :: prf_decl % "proof"
     1.5    and "supply" :: prf_script % "proof"
     1.6    and "using" "unfolding" :: prf_decl % "proof"
     1.7 -  and "fix" "assume" "presume" "define" "def" :: prf_asm % "proof"
     1.8 +  and "fix" "assume" "presume" "define" :: prf_asm % "proof"
     1.9    and "consider" :: prf_goal % "proof"
    1.10    and "obtain" :: prf_asm_goal % "proof"
    1.11    and "guess" :: prf_script_asm_goal % "proof"
    1.12 @@ -807,15 +807,6 @@
    1.13        >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
    1.14  
    1.15  val _ =
    1.16 -  Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
    1.17 -    (Parse.and_list1
    1.18 -      (Parse_Spec.opt_thm_name ":" --
    1.19 -        ((Parse.binding -- Parse.opt_mixfix) --
    1.20 -          ((@{keyword \<equiv>} || @{keyword ==}) |-- Parse.!!! Parse.termp)))
    1.21 -    >> (fn args => Toplevel.proof (fn state =>
    1.22 -        (legacy_feature "Old 'def' command -- use 'define' instead"; Proof.def_cmd args state))));
    1.23 -
    1.24 -val _ =
    1.25    Outer_Syntax.command @{command_keyword consider} "state cases rule"
    1.26      (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));
    1.27