# HG changeset patch # User blanchet # Date 1392640302 -3600 # Node ID 601ca8efa0006c883d3b0ade8ade5f154d9c75f0 # Parent 3dfb724db0996d5421092c3f80b273307caa4757 renamed 'datatype_new_compat' to 'datatype_compat' diff -r 3dfb724db099 -r 601ca8efa000 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Feb 17 13:31:42 2014 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Feb 17 13:31:42 2014 +0100 @@ -567,21 +567,21 @@ text {* \begin{matharray}{rcl} - @{command_def "datatype_new_compat"} & : & @{text "local_theory \ local_theory"} + @{command_def "datatype_compat"} & : & @{text "local_theory \ local_theory"} \end{matharray} @{rail \ - @@{command datatype_new_compat} (name +) + @@{command datatype_compat} (name +) \} \medskip \noindent -The @{command datatype_new_compat} command registers new-style datatypes as +The @{command datatype_compat} command registers new-style datatypes as old-style datatypes. For example: *} - datatype_new_compat even_nat odd_nat + datatype_compat even_nat odd_nat text {* \blankline *} @@ -626,7 +626,7 @@ the old \keyw{primrec} command. \end{itemize} -An alternative to @{command datatype_new_compat} is to use the old package's +An alternative to @{command datatype_compat} is to use the old package's \keyw{rep\_datatype} command. The associated proof obligations must then be discharged manually. *} @@ -966,7 +966,7 @@ \item \emph{The Standard ML interfaces are different.} Tools and extensions written to call the old ML interfaces will need to be adapted to the new interfaces. Little has been done so far in this direction. Whenever possible, it -is recommended to use @{command datatype_new_compat} or \keyw{rep\_datatype} +is recommended to use @{command datatype_compat} or \keyw{rep\_datatype} to register new-style datatypes as old-style datatypes. \item \emph{The constants @{text t_case} and @{text t_rec} are now called @@ -1126,12 +1126,12 @@ % The next example is defined using \keyw{fun} to escape the syntactic restrictions imposed on primitively recursive functions. The -@{command datatype_new_compat} command is needed to register new-style datatypes +@{command datatype_compat} command is needed to register new-style datatypes for use with \keyw{fun} and \keyw{function} (Section~\ref{sssec:datatype-new-compat}): *} - datatype_new_compat nat + datatype_compat nat text {* \blankline *} @@ -2714,7 +2714,7 @@ %* partial documentation % %* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them -% (for @{command datatype_new_compat} and prim(co)rec) +% (for @{command datatype_compat} and prim(co)rec) % % * a fortiori, no way to register same type as both data- and codatatype % diff -r 3dfb724db099 -r 601ca8efa000 src/HOL/BNF_Examples/ListF.thy --- a/src/HOL/BNF_Examples/ListF.thy Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/BNF_Examples/ListF.thy Mon Feb 17 13:31:42 2014 +0100 @@ -14,7 +14,7 @@ datatype_new 'a listF (map: mapF rel: relF) = NilF (defaults tlF: NilF) | Conss (hdF: 'a) (tlF: "'a listF") -datatype_new_compat listF +datatype_compat listF definition Singll ("[[_]]") where [simp]: "Singll a \ Conss a NilF" diff -r 3dfb724db099 -r 601ca8efa000 src/HOL/BNF_LFP.thy --- a/src/HOL/BNF_LFP.thy Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/BNF_LFP.thy Mon Feb 17 13:31:42 2014 +0100 @@ -13,7 +13,7 @@ imports BNF_FP_Base keywords "datatype_new" :: thy_decl and - "datatype_new_compat" :: thy_decl + "datatype_compat" :: thy_decl begin lemma subset_emptyI: "(\x. x \ A \ False) \ A \ {}" diff -r 3dfb724db099 -r 601ca8efa000 src/HOL/List.thy --- a/src/HOL/List.thy Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/List.thy Mon Feb 17 13:31:42 2014 +0100 @@ -11,8 +11,7 @@ datatype_new 'a list (map: map rel: list_all2) = =: Nil (defaults tl: "[]") ("[]") | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65) - -datatype_new_compat list +datatype_compat list lemma [case_names Nil Cons, cases type: list]: -- {* for backward compatibility -- names of variables differ *} diff -r 3dfb724db099 -r 601ca8efa000 src/HOL/Option.thy --- a/src/HOL/Option.thy Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Option.thy Mon Feb 17 13:31:42 2014 +0100 @@ -11,8 +11,7 @@ datatype_new 'a option = =: None | Some (the: 'a) - -datatype_new_compat option +datatype_compat option lemma [case_names None Some, cases type: option]: -- {* for backward compatibility -- names of variables differ *} diff -r 3dfb724db099 -r 601ca8efa000 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Feb 17 13:31:42 2014 +0100 @@ -355,7 +355,7 @@ end; (* These results are half broken. This is deliberate. We care only about those fields that are - used by "primrec", "primcorecursive", and "datatype_new_compat". *) + used by "primrec", "primcorecursive", and "datatype_compat". *) val fp_res = ({Ts = fpTs, bnfs = steal #bnfs, diff -r 3dfb724db099 -r 601ca8efa000 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Feb 17 13:31:42 2014 +0100 @@ -7,7 +7,7 @@ signature BNF_LFP_COMPAT = sig - val datatype_new_compat_cmd : string list -> local_theory -> local_theory + val datatype_compat_cmd : string list -> local_theory -> local_theory end; structure BNF_LFP_Compat : BNF_LFP_COMPAT = @@ -24,7 +24,7 @@ val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]}; (* TODO: graceful failure for local datatypes -- perhaps by making the command global *) -fun datatype_new_compat_cmd raw_fpT_names lthy = +fun datatype_compat_cmd raw_fpT_names lthy = let val thy = Proof_Context.theory_of lthy; @@ -203,8 +203,8 @@ end; val _ = - Outer_Syntax.local_theory @{command_spec "datatype_new_compat"} + Outer_Syntax.local_theory @{command_spec "datatype_compat"} "register new-style datatypes as old-style datatypes" - (Scan.repeat1 Parse.type_const >> datatype_new_compat_cmd); + (Scan.repeat1 Parse.type_const >> datatype_compat_cmd); end;