discontinued old 'def' command;
authorwenzelm
Sun Dec 03 13:22:09 2017 +0100 (7 weeks ago)
changeset 67119acb0807ddb56
parent 67118 ccab07d1196c
child 67120 491fd7f0b5df
discontinued old 'def' command;
NEWS
src/Doc/Isar_Ref/Proof.thy
src/FOL/ex/Locale_Test/Locale_Test1.thy
src/Pure/Isar/proof.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Sat Dec 02 16:50:53 2017 +0000
     1.2 +++ b/NEWS	Sun Dec 03 13:22:09 2017 +0100
     1.3 @@ -9,6 +9,10 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* The old 'def' command has been discontinued (legacy since
     1.8 +Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
     1.9 +object-logic equality or equivalence.
    1.10 +
    1.11  * Session-qualified theory names are mandatory: it is no longer possible
    1.12  to refer to unqualified theories from the parent session.
    1.13  INCOMPATIBILITY for old developments that have not been updated to
     2.1 --- a/src/Doc/Isar_Ref/Proof.thy	Sat Dec 02 16:50:53 2017 +0000
     2.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Sun Dec 03 13:22:09 2017 +0100
     2.3 @@ -128,7 +128,6 @@
     2.4      @{command_def "assume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     2.5      @{command_def "presume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     2.6      @{command_def "define"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     2.7 -    @{command_def "def"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     2.8    \end{matharray}
     2.9  
    2.10    The logical proof context consists of fixed variables and assumptions. The
    2.11 @@ -169,11 +168,6 @@
    2.12      ;
    2.13      @@{command define} @{syntax vars} @'where'
    2.14        (@{syntax props} + @'and') @{syntax for_fixes}
    2.15 -    ;
    2.16 -    @@{command def} (def + @'and')
    2.17 -    ;
    2.18 -    def: @{syntax thmdecl}? \<newline>
    2.19 -      @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
    2.20    \<close>}
    2.21  
    2.22    \<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary,
    2.23 @@ -207,9 +201,6 @@
    2.24    \<^medskip>
    2.25    It is also possible to abstract over local parameters as follows: \<^theory_text>\<open>define f
    2.26    :: "'a \<Rightarrow> 'b" where "f x = t" for x :: 'a\<close>.
    2.27 -
    2.28 -  \<^descr> \<^theory_text>\<open>def x \<equiv> t\<close> introduces a local (non-polymorphic) definition. This is an
    2.29 -  old form of \<^theory_text>\<open>define x where "x = t"\<close>.
    2.30  \<close>
    2.31  
    2.32  
     3.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Dec 02 16:50:53 2017 +0000
     3.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sun Dec 03 13:22:09 2017 +0100
     3.3 @@ -726,7 +726,7 @@
     3.4  
     3.5  end
     3.6  
     3.7 -sublocale lgrp < "def"?: dgrp
     3.8 +sublocale lgrp < def?: dgrp
     3.9    rewrites one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
    3.10  proof -
    3.11    show "dgrp(prod)" by unfold_locales
     4.1 --- a/src/Pure/Isar/proof.ML	Sat Dec 02 16:50:53 2017 +0000
     4.2 +++ b/src/Pure/Isar/proof.ML	Sun Dec 03 13:22:09 2017 +0100
     4.3 @@ -68,8 +68,6 @@
     4.4    val presume_cmd: (binding * string option * mixfix) list ->
     4.5      (string * string list) list list -> (Attrib.binding * (string * string list) list) list ->
     4.6      state -> state
     4.7 -  val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
     4.8 -  val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
     4.9    val chain: state -> state
    4.10    val chain_facts: thm list -> state -> state
    4.11    val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
    4.12 @@ -679,37 +677,6 @@
    4.13  end;
    4.14  
    4.15  
    4.16 -(* def *)
    4.17 -
    4.18 -local
    4.19 -
    4.20 -fun gen_def prep_att prep_var prep_binds args state =
    4.21 -  let
    4.22 -    val _ = assert_forward state;
    4.23 -    val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
    4.24 -    val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts;
    4.25 -  in
    4.26 -    state
    4.27 -    |> map_context_result (fold_map (fn (x, mx) => prep_var (x, NONE, mx)) raw_vars)
    4.28 -    |>> map (fn (x, _, mx) => (x, mx))
    4.29 -    |-> (fn vars =>
    4.30 -      map_context_result (prep_binds false (map swap raw_rhss))
    4.31 -      #-> (fn rhss =>
    4.32 -        let
    4.33 -          val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
    4.34 -            ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
    4.35 -        in map_context_result (Local_Defs.define defs) end))
    4.36 -    |-> (set_facts o map (#2 o #2))
    4.37 -  end;
    4.38 -
    4.39 -in
    4.40 -
    4.41 -val def = gen_def (K I) Proof_Context.cert_var Proof_Context.match_bind;
    4.42 -val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_var Proof_Context.match_bind_cmd;
    4.43 -
    4.44 -end;
    4.45 -
    4.46 -
    4.47  
    4.48  (** facts **)
    4.49  
     5.1 --- a/src/Pure/Pure.thy	Sat Dec 02 16:50:53 2017 +0000
     5.2 +++ b/src/Pure/Pure.thy	Sun Dec 03 13:22:09 2017 +0100
     5.3 @@ -55,7 +55,7 @@
     5.4    and "note" :: prf_decl % "proof"
     5.5    and "supply" :: prf_script % "proof"
     5.6    and "using" "unfolding" :: prf_decl % "proof"
     5.7 -  and "fix" "assume" "presume" "define" "def" :: prf_asm % "proof"
     5.8 +  and "fix" "assume" "presume" "define" :: prf_asm % "proof"
     5.9    and "consider" :: prf_goal % "proof"
    5.10    and "obtain" :: prf_asm_goal % "proof"
    5.11    and "guess" :: prf_script_asm_goal % "proof"
    5.12 @@ -807,15 +807,6 @@
    5.13        >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
    5.14  
    5.15  val _ =
    5.16 -  Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
    5.17 -    (Parse.and_list1
    5.18 -      (Parse_Spec.opt_thm_name ":" --
    5.19 -        ((Parse.binding -- Parse.opt_mixfix) --
    5.20 -          ((@{keyword \<equiv>} || @{keyword ==}) |-- Parse.!!! Parse.termp)))
    5.21 -    >> (fn args => Toplevel.proof (fn state =>
    5.22 -        (legacy_feature "Old 'def' command -- use 'define' instead"; Proof.def_cmd args state))));
    5.23 -
    5.24 -val _ =
    5.25    Outer_Syntax.command @{command_keyword consider} "state cases rule"
    5.26      (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));
    5.27