renamed 'datatype_new_compat' to 'datatype_compat'
authorblanchet
Mon Feb 17 13:31:42 2014 +0100 (2014-02-17)
changeset 55531601ca8efa000
parent 55530 3dfb724db099
child 55532 b751e6d7f4e9
renamed 'datatype_new_compat' to 'datatype_compat'
src/Doc/Datatypes/Datatypes.thy
src/HOL/BNF_Examples/ListF.thy
src/HOL/BNF_LFP.thy
src/HOL/List.thy
src/HOL/Option.thy
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Feb 17 13:31:42 2014 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Feb 17 13:31:42 2014 +0100
     1.3 @@ -567,21 +567,21 @@
     1.4  
     1.5  text {*
     1.6  \begin{matharray}{rcl}
     1.7 -  @{command_def "datatype_new_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}
     1.8 +  @{command_def "datatype_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}
     1.9  \end{matharray}
    1.10  
    1.11  @{rail \<open>
    1.12 -  @@{command datatype_new_compat} (name +)
    1.13 +  @@{command datatype_compat} (name +)
    1.14  \<close>}
    1.15  
    1.16  \medskip
    1.17  
    1.18  \noindent
    1.19 -The @{command datatype_new_compat} command registers new-style datatypes as
    1.20 +The @{command datatype_compat} command registers new-style datatypes as
    1.21  old-style datatypes. For example:
    1.22  *}
    1.23  
    1.24 -    datatype_new_compat even_nat odd_nat
    1.25 +    datatype_compat even_nat odd_nat
    1.26  
    1.27  text {* \blankline *}
    1.28  
    1.29 @@ -626,7 +626,7 @@
    1.30  the old \keyw{primrec} command.
    1.31  \end{itemize}
    1.32  
    1.33 -An alternative to @{command datatype_new_compat} is to use the old package's
    1.34 +An alternative to @{command datatype_compat} is to use the old package's
    1.35  \keyw{rep\_datatype} command. The associated proof obligations must then be
    1.36  discharged manually.
    1.37  *}
    1.38 @@ -966,7 +966,7 @@
    1.39  \item \emph{The Standard ML interfaces are different.} Tools and extensions
    1.40  written to call the old ML interfaces will need to be adapted to the new
    1.41  interfaces. Little has been done so far in this direction. Whenever possible, it
    1.42 -is recommended to use @{command datatype_new_compat} or \keyw{rep\_datatype}
    1.43 +is recommended to use @{command datatype_compat} or \keyw{rep\_datatype}
    1.44  to register new-style datatypes as old-style datatypes.
    1.45  
    1.46  \item \emph{The constants @{text t_case} and @{text t_rec} are now called
    1.47 @@ -1126,12 +1126,12 @@
    1.48  %
    1.49  The next example is defined using \keyw{fun} to escape the syntactic
    1.50  restrictions imposed on primitively recursive functions. The
    1.51 -@{command datatype_new_compat} command is needed to register new-style datatypes
    1.52 +@{command datatype_compat} command is needed to register new-style datatypes
    1.53  for use with \keyw{fun} and \keyw{function}
    1.54  (Section~\ref{sssec:datatype-new-compat}):
    1.55  *}
    1.56  
    1.57 -    datatype_new_compat nat
    1.58 +    datatype_compat nat
    1.59  
    1.60  text {* \blankline *}
    1.61  
    1.62 @@ -2714,7 +2714,7 @@
    1.63  %* partial documentation
    1.64  %
    1.65  %* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
    1.66 -%  (for @{command datatype_new_compat} and prim(co)rec)
    1.67 +%  (for @{command datatype_compat} and prim(co)rec)
    1.68  %
    1.69  %    * a fortiori, no way to register same type as both data- and codatatype
    1.70  %
     2.1 --- a/src/HOL/BNF_Examples/ListF.thy	Mon Feb 17 13:31:42 2014 +0100
     2.2 +++ b/src/HOL/BNF_Examples/ListF.thy	Mon Feb 17 13:31:42 2014 +0100
     2.3 @@ -14,7 +14,7 @@
     2.4  
     2.5  datatype_new 'a listF (map: mapF rel: relF) =
     2.6    NilF (defaults tlF: NilF) | Conss (hdF: 'a) (tlF: "'a listF")
     2.7 -datatype_new_compat listF
     2.8 +datatype_compat listF
     2.9  
    2.10  definition Singll ("[[_]]") where
    2.11    [simp]: "Singll a \<equiv> Conss a NilF"
     3.1 --- a/src/HOL/BNF_LFP.thy	Mon Feb 17 13:31:42 2014 +0100
     3.2 +++ b/src/HOL/BNF_LFP.thy	Mon Feb 17 13:31:42 2014 +0100
     3.3 @@ -13,7 +13,7 @@
     3.4  imports BNF_FP_Base
     3.5  keywords
     3.6    "datatype_new" :: thy_decl and
     3.7 -  "datatype_new_compat" :: thy_decl
     3.8 +  "datatype_compat" :: thy_decl
     3.9  begin
    3.10  
    3.11  lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
     4.1 --- a/src/HOL/List.thy	Mon Feb 17 13:31:42 2014 +0100
     4.2 +++ b/src/HOL/List.thy	Mon Feb 17 13:31:42 2014 +0100
     4.3 @@ -11,8 +11,7 @@
     4.4  datatype_new 'a list (map: map rel: list_all2) =
     4.5      =: Nil (defaults tl: "[]")  ("[]")
     4.6    | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
     4.7 -
     4.8 -datatype_new_compat list
     4.9 +datatype_compat list
    4.10  
    4.11  lemma [case_names Nil Cons, cases type: list]:
    4.12    -- {* for backward compatibility -- names of variables differ *}
     5.1 --- a/src/HOL/Option.thy	Mon Feb 17 13:31:42 2014 +0100
     5.2 +++ b/src/HOL/Option.thy	Mon Feb 17 13:31:42 2014 +0100
     5.3 @@ -11,8 +11,7 @@
     5.4  datatype_new 'a option =
     5.5      =: None
     5.6    | Some (the: 'a)
     5.7 -
     5.8 -datatype_new_compat option
     5.9 +datatype_compat option
    5.10  
    5.11  lemma [case_names None Some, cases type: option]:
    5.12    -- {* for backward compatibility -- names of variables differ *}
     6.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Feb 17 13:31:42 2014 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Feb 17 13:31:42 2014 +0100
     6.3 @@ -355,7 +355,7 @@
     6.4        end;
     6.5  
     6.6      (* These results are half broken. This is deliberate. We care only about those fields that are
     6.7 -       used by "primrec", "primcorecursive", and "datatype_new_compat". *)
     6.8 +       used by "primrec", "primcorecursive", and "datatype_compat". *)
     6.9      val fp_res =
    6.10        ({Ts = fpTs,
    6.11          bnfs = steal #bnfs,
     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Feb 17 13:31:42 2014 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Feb 17 13:31:42 2014 +0100
     7.3 @@ -7,7 +7,7 @@
     7.4  
     7.5  signature BNF_LFP_COMPAT =
     7.6  sig
     7.7 -  val datatype_new_compat_cmd : string list -> local_theory -> local_theory
     7.8 +  val datatype_compat_cmd : string list -> local_theory -> local_theory
     7.9  end;
    7.10  
    7.11  structure BNF_LFP_Compat : BNF_LFP_COMPAT =
    7.12 @@ -24,7 +24,7 @@
    7.13  val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
    7.14  
    7.15  (* TODO: graceful failure for local datatypes -- perhaps by making the command global *)
    7.16 -fun datatype_new_compat_cmd raw_fpT_names lthy =
    7.17 +fun datatype_compat_cmd raw_fpT_names lthy =
    7.18    let
    7.19      val thy = Proof_Context.theory_of lthy;
    7.20  
    7.21 @@ -203,8 +203,8 @@
    7.22    end;
    7.23  
    7.24  val _ =
    7.25 -  Outer_Syntax.local_theory @{command_spec "datatype_new_compat"}
    7.26 +  Outer_Syntax.local_theory @{command_spec "datatype_compat"}
    7.27      "register new-style datatypes as old-style datatypes"
    7.28 -    (Scan.repeat1 Parse.type_const >> datatype_new_compat_cmd);
    7.29 +    (Scan.repeat1 Parse.type_const >> datatype_compat_cmd);
    7.30  
    7.31  end;