updated news
authorblanchet
Thu Sep 11 19:32:36 2014 +0200 (2014-09-11)
changeset 5831091ea607a34d8
parent 58309 a09ec6daaa19
child 58311 a684dd412115
updated news
NEWS
src/Doc/Codegen/Evaluation.thy
src/Doc/Codegen/Introduction.thy
src/Doc/Codegen/Refinement.thy
src/Doc/Datatypes/Datatypes.thy
src/Doc/Datatypes/document/root.tex
src/Doc/Functions/Functions.thy
src/Doc/Isar_Ref/Generic.thy
src/Doc/Isar_Ref/HOL_Specific.thy
src/Doc/Isar_Ref/Synopsis.thy
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Smartcard/EventSC.thy
src/HOL/Auth/TLS.thy
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/Name.thy
src/HOL/Bali/State.thy
src/HOL/Bali/Term.thy
src/HOL/Bali/Type.thy
src/HOL/Bali/Value.thy
src/HOL/Code_Evaluation.thy
src/HOL/Codegenerator_Test/Code_Test.thy
src/HOL/Datatype_Examples/Compat.thy
src/HOL/Datatype_Examples/IsaFoR_Datatypes.thy
src/HOL/Datatype_Examples/Lambda_Term.thy
src/HOL/Datatype_Examples/Misc_Datatype.thy
src/HOL/Datatype_Examples/Process.thy
src/HOL/Datatype_Examples/Stream_Processor.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Commutative_Ring.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Enum.thy
src/HOL/Extraction.thy
src/HOL/HOLCF/Discrete.thy
src/HOL/HOLCF/FOCUS/Buffer.thy
src/HOL/HOLCF/IOA/ABP/Abschannel.thy
src/HOL/HOLCF/IOA/ABP/Action.thy
src/HOL/HOLCF/IOA/NTP/Abschannel.thy
src/HOL/HOLCF/IOA/NTP/Action.thy
src/HOL/HOLCF/IOA/Storage/Action.thy
src/HOL/HOLCF/IOA/ex/TrivEx.thy
src/HOL/HOLCF/IOA/ex/TrivEx2.thy
src/HOL/HOLCF/Up.thy
src/HOL/Hoare/Heap.thy
src/HOL/Hoare/Hoare_Logic.thy
src/HOL/Hoare/Hoare_Logic_Abort.thy
src/HOL/Hoare_Parallel/Graph.thy
src/HOL/Hoare_Parallel/OG_Com.thy
src/HOL/Hoare_Parallel/RG_Com.thy
src/HOL/IMP/ACom.thy
src/HOL/IMP/AExp.thy
src/HOL/IMP/ASM.thy
src/HOL/IMP/Abs_Int1_const.thy
src/HOL/IMP/Abs_Int1_parity.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy
src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy
src/HOL/IMP/BExp.thy
src/HOL/IMP/C_like.thy
src/HOL/IMP/Com.thy
src/HOL/IMP/Compiler.thy
src/HOL/IMP/OO.thy
src/HOL/IMP/Poly_Types.thy
src/HOL/IMP/Procs.thy
src/HOL/IMP/Types.thy
src/HOL/IMP/VCG.thy
src/HOL/IMPP/Com.thy
src/HOL/IMPP/Hoare.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/ex/SatChecker.thy
src/HOL/Induct/ABexp.thy
src/HOL/Induct/Com.thy
src/HOL/Induct/Comb.thy
src/HOL/Induct/Common_Patterns.thy
src/HOL/Induct/Ordinals.thy
src/HOL/Induct/PropLog.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Induct/Term.thy
src/HOL/Induct/Tree.thy
src/HOL/Isar_Examples/Expr_Compiler.thy
src/HOL/Isar_Examples/Hoare.thy
src/HOL/Isar_Examples/Nested_Datatype.thy
src/HOL/Lattice/Orders.thy
src/HOL/Lazy_Sequence.thy
src/HOL/Library/Extended.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/IArray.thy
src/HOL/Library/Lattice_Constructions.thy
src/HOL/Library/Parallel.thy
src/HOL/Library/Phantom_Type.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Library/Tree.thy
src/HOL/List.thy
src/HOL/Metis_Examples/Binary_Tree.thy
src/HOL/Metis_Examples/Message.thy
src/HOL/Metis_Examples/Trans_Closure.thy
src/HOL/MicroJava/DFA/Err.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/Term.thy
src/HOL/MicroJava/J/Type.thy
src/HOL/MicroJava/J/Value.thy
src/HOL/MicroJava/JVM/JVMDefensive.thy
src/HOL/MicroJava/JVM/JVMInstructions.thy
src/HOL/NanoJava/Decl.thy
src/HOL/NanoJava/State.thy
src/HOL/NanoJava/Term.thy
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Datatype_Nits.thy
src/HOL/Nitpick_Examples/Integer_Nits.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Nitpick_Examples/Refute_Nits.thy
src/HOL/Nominal/Examples/CK_Machine.thy
src/HOL/Nominal/Examples/Pattern.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Num.thy
src/HOL/Option.thy
src/HOL/Predicate.thy
src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
src/HOL/Predicate_Compile_Examples/Examples.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
src/HOL/Predicate_Compile_Examples/IMP_1.thy
src/HOL/Predicate_Compile_Examples/IMP_2.thy
src/HOL/Predicate_Compile_Examples/IMP_3.thy
src/HOL/Predicate_Compile_Examples/IMP_4.thy
src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
src/HOL/Proofs/Extraction/Higman.thy
src/HOL/Proofs/Extraction/Warshall.thy
src/HOL/Proofs/Lambda/Lambda.thy
src/HOL/Proofs/Lambda/LambdaType.thy
src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
src/HOL/Quickcheck_Examples/Hotel_Example.thy
src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Quotient_Examples/Quotient_Message.thy
src/HOL/Record.thy
src/HOL/SET_Protocol/Event_SET.thy
src/HOL/SET_Protocol/Message_SET.thy
src/HOL/SPARK/Manual/Complex_Types.thy
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/String.thy
src/HOL/TLA/Inc/Inc.thy
src/HOL/TLA/Memory/MemClerkParameters.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/Memory/MemoryParameters.thy
src/HOL/TLA/Memory/RPCParameters.thy
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Typerep.thy
src/HOL/UNITY/Comp/Counter.thy
src/HOL/UNITY/Simple/Network.thy
src/HOL/UNITY/Simple/Token.thy
src/HOL/Unix/Nested_Environment.thy
src/HOL/Unix/Unix.thy
src/HOL/ex/Adhoc_Overloading_Examples.thy
src/HOL/ex/BT.thy
src/HOL/ex/Chinese.thy
src/HOL/ex/Eval_Examples.thy
src/HOL/ex/Fundefs.thy
src/HOL/ex/Hebrew.thy
src/HOL/ex/Normalization_by_Evaluation.thy
src/HOL/ex/Records.thy
src/HOL/ex/Reflection_Examples.thy
src/HOL/ex/Refute_Examples.thy
src/HOL/ex/Seq.thy
src/HOL/ex/Serbian.thy
src/HOL/ex/Sudoku.thy
src/HOL/ex/Termination.thy
src/HOL/ex/Transitive_Closure_Table_Ex.thy
src/HOL/ex/Tree23.thy
src/HOL/ex/Unification.thy
     1.1 --- a/NEWS	Thu Sep 11 19:26:59 2014 +0200
     1.2 +++ b/NEWS	Thu Sep 11 19:32:36 2014 +0200
     1.3 @@ -28,6 +28,9 @@
     1.4  Minor INCOMPATIBILITY.
     1.5  
     1.6  * New (co)datatype package:
     1.7 +  - The 'datatype_new' command has been renamed 'datatype'. The old command of
     1.8 +    that name is now called 'old_datatype'. See 'isabelle doc datatypes' for
     1.9 +    information on porting.
    1.10    - Renamed theorems:
    1.11        disc_corec ~> corec_disc
    1.12        disc_corec_iff ~> corec_disc_iff
    1.13 @@ -58,6 +61,9 @@
    1.14      INCOMPATIBILITY.
    1.15  
    1.16  * Old datatype package:
    1.17 +  - The old 'datatype' command has been renamed 'old_datatype', and
    1.18 +    'rep_datatype' has been renamed 'old_rep_datatype'. See
    1.19 +    'isabelle doc datatypes' for information on porting.
    1.20    - Renamed theorems:
    1.21        weak_case_cong ~> case_cong_weak
    1.22      INCOMPATIBILITY.
     2.1 --- a/src/Doc/Codegen/Evaluation.thy	Thu Sep 11 19:26:59 2014 +0200
     2.2 +++ b/src/Doc/Codegen/Evaluation.thy	Thu Sep 11 19:32:36 2014 +0200
     2.3 @@ -205,7 +205,7 @@
     2.4    An simplistic example:
     2.5  *}
     2.6  
     2.7 -datatype_new %quote form_ord = T | F | Less nat nat
     2.8 +datatype %quote form_ord = T | F | Less nat nat
     2.9    | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
    2.10  
    2.11  primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
    2.12 @@ -259,7 +259,7 @@
    2.13    example:
    2.14  *}
    2.15  
    2.16 -datatype_new %quote form = T | F | And form form | Or form form (*<*)
    2.17 +datatype %quote form = T | F | And form form | Or form form (*<*)
    2.18  
    2.19  (*>*) ML %quotett {*
    2.20    fun eval_form @{code T} = true
     3.1 --- a/src/Doc/Codegen/Introduction.thy	Thu Sep 11 19:26:59 2014 +0200
     3.2 +++ b/src/Doc/Codegen/Introduction.thy	Thu Sep 11 19:32:36 2014 +0200
     3.3 @@ -35,7 +35,7 @@
     3.4  subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *}
     3.5  
     3.6  text {*
     3.7 -  In a HOL theory, the @{command_def datatype_new} and @{command_def
     3.8 +  In a HOL theory, the @{command_def datatype} and @{command_def
     3.9    definition}/@{command_def primrec}/@{command_def fun} declarations
    3.10    form the core of a functional programming language.  By default
    3.11    equational theorems stemming from those are used for generated code,
    3.12 @@ -45,7 +45,7 @@
    3.13    For example, here a simple \qt{implementation} of amortised queues:
    3.14  *}
    3.15  
    3.16 -datatype_new %quote 'a queue = AQueue "'a list" "'a list"
    3.17 +datatype %quote 'a queue = AQueue "'a list" "'a list"
    3.18  
    3.19  definition %quote empty :: "'a queue" where
    3.20    "empty = AQueue [] []"
     4.1 --- a/src/Doc/Codegen/Refinement.thy	Thu Sep 11 19:26:59 2014 +0200
     4.2 +++ b/src/Doc/Codegen/Refinement.thy	Thu Sep 11 19:32:36 2014 +0200
     4.3 @@ -87,7 +87,7 @@
     4.4    queues:
     4.5  *}
     4.6  
     4.7 -datatype_new %quote 'a queue = Queue "'a list"
     4.8 +datatype %quote 'a queue = Queue "'a list"
     4.9  
    4.10  definition %quote empty :: "'a queue" where
    4.11    "empty = Queue []"
     5.1 --- a/src/Doc/Datatypes/Datatypes.thy	Thu Sep 11 19:26:59 2014 +0200
     5.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 11 19:32:36 2014 +0200
     5.3 @@ -28,7 +28,7 @@
     5.4  through a large class of non-datatypes, such as finite sets:
     5.5  *}
     5.6  
     5.7 -    datatype_new 'a tree\<^sub>f\<^sub>s = Node\<^sub>f\<^sub>s (lbl\<^sub>f\<^sub>s: 'a) (sub\<^sub>f\<^sub>s: "'a tree\<^sub>f\<^sub>s fset")
     5.8 +    datatype 'a tree\<^sub>f\<^sub>s = Node\<^sub>f\<^sub>s (lbl\<^sub>f\<^sub>s: 'a) (sub\<^sub>f\<^sub>s: "'a tree\<^sub>f\<^sub>s fset")
     5.9  
    5.10  text {*
    5.11  \noindent
    5.12 @@ -37,7 +37,7 @@
    5.13  
    5.14      context linorder
    5.15      begin
    5.16 -    datatype_new flag = Less | Eq | Greater
    5.17 +    datatype flag = Less | Eq | Greater
    5.18      end
    5.19  
    5.20  text {*
    5.21 @@ -64,8 +64,8 @@
    5.22  following four Rose tree examples:
    5.23  *}
    5.24  
    5.25 -    datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
    5.26 -    datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
    5.27 +    datatype (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
    5.28 +    datatype (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
    5.29      codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f 'a "'a tree\<^sub>i\<^sub>f list"
    5.30      codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
    5.31  
    5.32 @@ -96,7 +96,7 @@
    5.33  \setlength{\itemsep}{0pt}
    5.34  
    5.35  \item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,''
    5.36 -describes how to specify datatypes using the @{command datatype_new} command.
    5.37 +describes how to specify datatypes using the @{command datatype} command.
    5.38  
    5.39  \item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
    5.40  Functions,'' describes how to specify recursive functions using
    5.41 @@ -118,7 +118,7 @@
    5.42  ``Deriving Destructors and Theorems for Free Constructors,'' explains how to
    5.43  use the command @{command free_constructors} to derive destructor constants
    5.44  and theorems for freely generated types, as performed internally by @{command
    5.45 -datatype_new} and @{command codatatype}.
    5.46 +datatype} and @{command codatatype}.
    5.47  
    5.48  %\item Section \ref{sec:using-the-standard-ml-interface}, ``Using the Standard
    5.49  ML Interface,'' %describes the package's programmatic interface.
    5.50 @@ -156,7 +156,7 @@
    5.51    \label{sec:defining-datatypes} *}
    5.52  
    5.53  text {*
    5.54 -Datatypes can be specified using the @{command datatype_new} command.
    5.55 +Datatypes can be specified using the @{command datatype} command.
    5.56  *}
    5.57  
    5.58  
    5.59 @@ -179,7 +179,7 @@
    5.60  All their constructors are nullary:
    5.61  *}
    5.62  
    5.63 -    datatype_new trool = Truue | Faalse | Perhaaps
    5.64 +    datatype trool = Truue | Faalse | Perhaaps
    5.65  
    5.66  text {*
    5.67  \noindent
    5.68 @@ -193,7 +193,7 @@
    5.69      hide_const None Some map_option
    5.70      hide_type option
    5.71  (*>*)
    5.72 -    datatype_new 'a option = None | Some 'a
    5.73 +    datatype 'a option = None | Some 'a
    5.74  
    5.75  text {*
    5.76  \noindent
    5.77 @@ -203,7 +203,7 @@
    5.78  The next example has three type parameters:
    5.79  *}
    5.80  
    5.81 -    datatype_new ('a, 'b, 'c) triple = Triple 'a 'b 'c
    5.82 +    datatype ('a, 'b, 'c) triple = Triple 'a 'b 'c
    5.83  
    5.84  text {*
    5.85  \noindent
    5.86 @@ -213,7 +213,7 @@
    5.87  is also possible:
    5.88  *}
    5.89  
    5.90 -    datatype_new ('a, 'b, 'c) triple\<^sub>u = Triple\<^sub>u "'a * 'b * 'c"
    5.91 +    datatype ('a, 'b, 'c) triple\<^sub>u = Triple\<^sub>u "'a * 'b * 'c"
    5.92  
    5.93  text {*
    5.94  \noindent
    5.95 @@ -229,7 +229,7 @@
    5.96  Natural numbers are the simplest example of a recursive type:
    5.97  *}
    5.98  
    5.99 -    datatype_new nat = Zero | Succ nat
   5.100 +    datatype nat = Zero | Succ nat
   5.101  
   5.102  text {*
   5.103  \noindent
   5.104 @@ -237,7 +237,7 @@
   5.105  stores a value of type @{typ 'b} at the very end:
   5.106  *}
   5.107  
   5.108 -    datatype_new (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
   5.109 +    datatype (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
   5.110  
   5.111  
   5.112  subsubsection {* Mutual Recursion
   5.113 @@ -249,7 +249,7 @@
   5.114  natural numbers:
   5.115  *}
   5.116  
   5.117 -    datatype_new even_nat = Even_Zero | Even_Succ odd_nat
   5.118 +    datatype even_nat = Even_Zero | Even_Succ odd_nat
   5.119      and odd_nat = Odd_Succ even_nat
   5.120  
   5.121  text {*
   5.122 @@ -258,7 +258,7 @@
   5.123  expressions:
   5.124  *}
   5.125  
   5.126 -    datatype_new ('a, 'b) exp =
   5.127 +    datatype ('a, 'b) exp =
   5.128        Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
   5.129      and ('a, 'b) trm =
   5.130        Factor "('a, 'b) fct" | Prod "('a, 'b) fct" "('a, 'b) trm"
   5.131 @@ -276,7 +276,7 @@
   5.132  follows:
   5.133  *}
   5.134  
   5.135 -    datatype_new 'a btree =
   5.136 +    datatype 'a btree =
   5.137        BNode 'a "'a btree option" "'a btree option"
   5.138  
   5.139  text {*
   5.140 @@ -284,7 +284,7 @@
   5.141  Not all nestings are admissible. For example, this command will fail:
   5.142  *}
   5.143  
   5.144 -    datatype_new 'a wrong = W1 | W2 (*<*)'a
   5.145 +    datatype 'a wrong = W1 | W2 (*<*)'a
   5.146      typ (*>*)"'a wrong \<Rightarrow> 'a"
   5.147  
   5.148  text {*
   5.149 @@ -294,8 +294,8 @@
   5.150  datatypes defined in terms of~@{text "\<Rightarrow>"}:
   5.151  *}
   5.152  
   5.153 -    datatype_new ('a, 'b) fun_copy = Fun "'a \<Rightarrow> 'b"
   5.154 -    datatype_new 'a also_wrong = W1 | W2 (*<*)'a
   5.155 +    datatype ('a, 'b) fun_copy = Fun "'a \<Rightarrow> 'b"
   5.156 +    datatype 'a also_wrong = W1 | W2 (*<*)'a
   5.157      typ (*>*)"('a also_wrong, 'a) fun_copy"
   5.158  
   5.159  text {*
   5.160 @@ -303,14 +303,14 @@
   5.161  The following definition of @{typ 'a}-branching trees is legal:
   5.162  *}
   5.163  
   5.164 -    datatype_new 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
   5.165 +    datatype 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
   5.166  
   5.167  text {*
   5.168  \noindent
   5.169  And so is the definition of hereditarily finite sets:
   5.170  *}
   5.171  
   5.172 -    datatype_new hfset = HFSet "hfset fset"
   5.173 +    datatype hfset = HFSet "hfset fset"
   5.174  
   5.175  text {*
   5.176  \noindent
   5.177 @@ -323,15 +323,15 @@
   5.178  
   5.179  Type constructors must be registered as BNFs to have live arguments. This is
   5.180  done automatically for datatypes and codatatypes introduced by the @{command
   5.181 -datatype_new} and @{command codatatype} commands.
   5.182 +datatype} and @{command codatatype} commands.
   5.183  Section~\ref{sec:introducing-bounded-natural-functors} explains how to
   5.184  register arbitrary type constructors as BNFs.
   5.185  
   5.186  Here is another example that fails:
   5.187  *}
   5.188  
   5.189 -    datatype_new 'a pow_list = PNil 'a (*<*)'a
   5.190 -    datatype_new 'a pow_list' = PNil' 'a (*>*)| PCons "('a * 'a) pow_list"
   5.191 +    datatype 'a pow_list = PNil 'a (*<*)'a
   5.192 +    datatype 'a pow_list' = PNil' 'a (*>*)| PCons "('a * 'a) pow_list"
   5.193  
   5.194  text {*
   5.195  \noindent
   5.196 @@ -345,7 +345,7 @@
   5.197    \label{sssec:datatype-auxiliary-constants-and-properties} *}
   5.198  
   5.199  text {*
   5.200 -The @{command datatype_new} command introduces various constants in addition to
   5.201 +The @{command datatype} command introduces various constants in addition to
   5.202  the constructors. With each datatype are associated set functions, a map
   5.203  function, a relator, discriminators, and selectors, all of which can be given
   5.204  custom names. In the example below, the familiar names @{text null}, @{text hd},
   5.205 @@ -368,7 +368,7 @@
   5.206  
   5.207      context early begin
   5.208  (*>*)
   5.209 -    datatype_new (set: 'a) list =
   5.210 +    datatype (set: 'a) list =
   5.211        null: Nil
   5.212      | Cons (hd: 'a) (tl: "'a list")
   5.213      for
   5.214 @@ -433,11 +433,11 @@
   5.215  (*<*)
   5.216      end
   5.217  (*>*)
   5.218 -    datatype_new ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
   5.219 +    datatype ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
   5.220  
   5.221  text {* \blankline *}
   5.222  
   5.223 -    datatype_new (set: 'a) list =
   5.224 +    datatype (set: 'a) list =
   5.225        null: Nil ("[]")
   5.226      | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
   5.227      for
   5.228 @@ -461,16 +461,16 @@
   5.229  subsection {* Command Syntax
   5.230    \label{ssec:datatype-command-syntax} *}
   5.231  
   5.232 -subsubsection {* \keyw{datatype_new}
   5.233 +subsubsection {* \keyw{datatype}
   5.234    \label{sssec:datatype-new} *}
   5.235  
   5.236  text {*
   5.237  \begin{matharray}{rcl}
   5.238 -  @{command_def "datatype_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
   5.239 +  @{command_def "datatype"} & : & @{text "local_theory \<rightarrow> local_theory"}
   5.240  \end{matharray}
   5.241  
   5.242  @{rail \<open>
   5.243 -  @@{command datatype_new} target? @{syntax dt_options}? \<newline>
   5.244 +  @@{command datatype} target? @{syntax dt_options}? \<newline>
   5.245      (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \<newline>
   5.246       @{syntax map_rel}? (@'where' (prop + '|'))? + @'and')
   5.247    ;
   5.248 @@ -484,7 +484,7 @@
   5.249  \medskip
   5.250  
   5.251  \noindent
   5.252 -The @{command datatype_new} command introduces a set of mutually recursive
   5.253 +The @{command datatype} command introduces a set of mutually recursive
   5.254  datatypes specified by their constructors.
   5.255  
   5.256  The syntactic entity \synt{target} can be used to specify a local
   5.257 @@ -667,7 +667,7 @@
   5.258    \label{ssec:datatype-generated-theorems} *}
   5.259  
   5.260  text {*
   5.261 -The characteristic theorems generated by @{command datatype_new} are grouped in
   5.262 +The characteristic theorems generated by @{command datatype} are grouped in
   5.263  three broad categories:
   5.264  
   5.265  \begin{itemize}
   5.266 @@ -1009,7 +1009,7 @@
   5.267  \end{indentblock}
   5.268  
   5.269  \noindent
   5.270 -For convenience, @{command datatype_new} also provides the following collection:
   5.271 +For convenience, @{command datatype} also provides the following collection:
   5.272  
   5.273  \begin{indentblock}
   5.274  \begin{description}
   5.275 @@ -1026,7 +1026,7 @@
   5.276    \label{ssec:datatype-compatibility-issues} *}
   5.277  
   5.278  text {*
   5.279 -The command @{command datatype_new} has been designed to be highly compatible
   5.280 +The command @{command datatype} has been designed to be highly compatible
   5.281  with the old command (which is now called \keyw{old_datatype}), to ease
   5.282  migration. There are nonetheless a few incompatibilities that may arise when
   5.283  porting:
   5.284 @@ -1268,7 +1268,7 @@
   5.285  *}
   5.286  
   5.287  (*<*)
   5.288 -    datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f (lbl\<^sub>f\<^sub>f: 'a) (sub\<^sub>f\<^sub>f: "'a tree\<^sub>f\<^sub>f list")
   5.289 +    datatype 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f (lbl\<^sub>f\<^sub>f: 'a) (sub\<^sub>f\<^sub>f: "'a tree\<^sub>f\<^sub>f list")
   5.290  (*>*)
   5.291      primrec at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
   5.292        "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
   5.293 @@ -1322,7 +1322,7 @@
   5.294  $n = 2$:
   5.295  *}
   5.296  
   5.297 -    datatype_new 'a ftree2 = FTLeaf2 'a | FTNode2 "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2"
   5.298 +    datatype 'a ftree2 = FTLeaf2 'a | FTNode2 "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2"
   5.299  
   5.300  text {* \blankline *}
   5.301  
   5.302 @@ -1533,7 +1533,7 @@
   5.303  
   5.304  text {* \blankline *}
   5.305  
   5.306 -    datatype_new ('a, 'b) tlist =
   5.307 +    datatype ('a, 'b) tlist =
   5.308        TNil (termi: 'b)
   5.309      | TCons (thd: 'a) (ttl: "('a, 'b) tlist")
   5.310      where
   5.311 @@ -2455,7 +2455,7 @@
   5.312  lazy lists. The cardinal bound limits the number of elements returned by the
   5.313  set function; it may not depend on the cardinality of @{typ 'a}.
   5.314  
   5.315 -The type constructors introduced by @{command datatype_new} and
   5.316 +The type constructors introduced by @{command datatype} and
   5.317  @{command codatatype} are automatically registered as BNFs. In addition, a
   5.318  number of old-style datatypes and non-free types are preregistered.
   5.319  
   5.320 @@ -2653,7 +2653,7 @@
   5.321  @{text dead} in front of the type variable (e.g., @{text "(dead 'a)"})
   5.322  instead of an identifier for the corresponding set function. Witnesses can be
   5.323  specified by their types. Otherwise, the syntax of @{command bnf_axiomatization}
   5.324 -is identical to the left-hand side of a @{command datatype_new} or
   5.325 +is identical to the left-hand side of a @{command datatype} or
   5.326  @{command codatatype} definition.
   5.327  
   5.328  The command is useful to reason abstractly about BNFs. The axioms are safe
   5.329 @@ -2682,7 +2682,7 @@
   5.330  
   5.331  text {*
   5.332  The derivation of convenience theorems for types equipped with free constructors,
   5.333 -as performed internally by @{command datatype_new} and @{command codatatype},
   5.334 +as performed internally by @{command datatype} and @{command codatatype},
   5.335  is available as a stand-alone command called @{command free_constructors}.
   5.336  
   5.337  %  * need for this is rare but may arise if you want e.g. to add destructors to
   5.338 @@ -2731,7 +2731,7 @@
   5.339  \synt{name} denotes an identifier, \synt{prop} denotes a HOL proposition, and
   5.340  \synt{term} denotes a HOL term \cite{isabelle-isar-ref}.
   5.341  
   5.342 -The syntax resembles that of @{command datatype_new} and @{command codatatype}
   5.343 +The syntax resembles that of @{command datatype} and @{command codatatype}
   5.344  definitions (Sections
   5.345  \ref{ssec:datatype-command-syntax}~and~\ref{ssec:codatatype-command-syntax}).
   5.346  A constructor is specified by an optional name for the discriminator, the
   5.347 @@ -2761,13 +2761,13 @@
   5.348  Plugins extend the (co)datatype package to interoperate with other Isabelle
   5.349  packages and tools, such as the code generator, Transfer, Lifting, and
   5.350  Quickcheck. They can be enabled or disabled individually using the
   5.351 -@{syntax plugins} option to the commands @{command datatype_new},
   5.352 +@{syntax plugins} option to the commands @{command datatype},
   5.353  @{command codatatype}, @{command free_constructors}, @{command bnf}, and
   5.354  @{command bnf_axiomatization}.
   5.355  For example:
   5.356  *}
   5.357  
   5.358 -    datatype_new (plugins del: code "quickcheck_*") color = Red | Black
   5.359 +    datatype (plugins del: code "quickcheck_*") color = Red | Black
   5.360  
   5.361  
   5.362  subsection {* Code Generator
     6.1 --- a/src/Doc/Datatypes/document/root.tex	Thu Sep 11 19:26:59 2014 +0200
     6.2 +++ b/src/Doc/Datatypes/document/root.tex	Thu Sep 11 19:32:36 2014 +0200
     6.3 @@ -77,7 +77,7 @@
     6.4  \begin{abstract}
     6.5  \noindent
     6.6  This tutorial describes the definitional package for datatypes and codatatypes
     6.7 -in Isabelle/HOL. The package provides four main commands: \keyw{datatype_new},
     6.8 +in Isabelle/HOL. The package provides four main commands: \keyw{datatype},
     6.9  \keyw{codatatype}, \keyw{primrec}, and \keyw{primcorec}.
    6.10  \end{abstract}
    6.11  
     7.1 --- a/src/Doc/Functions/Functions.thy	Thu Sep 11 19:26:59 2014 +0200
     7.2 +++ b/src/Doc/Functions/Functions.thy	Thu Sep 11 19:32:36 2014 +0200
     7.3 @@ -522,7 +522,7 @@
     7.4    and @{term "X"} for true, false and uncertain propositions, respectively. 
     7.5  *}
     7.6  
     7.7 -datatype_new P3 = T | F | X
     7.8 +datatype P3 = T | F | X
     7.9  
    7.10  text {* \noindent Then the conjunction of such values can be defined as follows: *}
    7.11  
    7.12 @@ -1122,7 +1122,7 @@
    7.13    As an example, imagine a datatype of n-ary trees:
    7.14  *}
    7.15  
    7.16 -datatype_new 'a tree = 
    7.17 +datatype 'a tree = 
    7.18    Leaf 'a 
    7.19  | Branch "'a tree list"
    7.20  
     8.1 --- a/src/Doc/Isar_Ref/Generic.thy	Thu Sep 11 19:26:59 2014 +0200
     8.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Thu Sep 11 19:32:36 2014 +0200
     8.3 @@ -736,7 +736,7 @@
     8.4    monotonically through the theory hierarchy: forming a new theory,
     8.5    the union of the simpsets of its imports are taken as starting
     8.6    point.  Also note that definitional packages like @{command
     8.7 -  "datatype_new"}, @{command "primrec"}, @{command "fun"} routinely
     8.8 +  "datatype"}, @{command "primrec"}, @{command "fun"} routinely
     8.9    declare Simplifier rules to the target context, while plain
    8.10    @{command "definition"} is an exception in \emph{not} declaring
    8.11    anything.
     9.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Sep 11 19:26:59 2014 +0200
     9.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Sep 11 19:32:36 2014 +0200
     9.3 @@ -283,7 +283,7 @@
     9.4    \begin{description}
     9.5  
     9.6    \item @{command (HOL) "primrec"} defines primitive recursive
     9.7 -  functions over datatypes (see also @{command_ref (HOL) datatype_new}).
     9.8 +  functions over datatypes (see also @{command_ref (HOL) datatype}).
     9.9    The given @{text equations} specify reduction rules that are produced
    9.10    by instantiating the generic combinator for primitive recursion that
    9.11    is available for each datatype.
    9.12 @@ -378,7 +378,7 @@
    9.13    boolean expressions, and use @{command primrec} for evaluation
    9.14    functions that follow the same recursive structure. *}
    9.15  
    9.16 -datatype_new 'a aexp =
    9.17 +datatype 'a aexp =
    9.18      IF "'a bexp"  "'a aexp"  "'a aexp"
    9.19    | Sum "'a aexp"  "'a aexp"
    9.20    | Diff "'a aexp"  "'a aexp"
    9.21 @@ -449,7 +449,7 @@
    9.22  text {* Functions on datatypes with nested recursion are also defined
    9.23    by mutual primitive recursion. *}
    9.24  
    9.25 -datatype_new ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
    9.26 +datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
    9.27  
    9.28  text {* A substitution function on type @{typ "('a, 'b) term"} can be
    9.29    defined as follows, by working simultaneously on @{typ "('a, 'b)
    9.30 @@ -479,7 +479,7 @@
    9.31    primitive recursion is just as easy.
    9.32  *}
    9.33  
    9.34 -datatype_new 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
    9.35 +datatype 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
    9.36  
    9.37  primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
    9.38  where
    9.39 @@ -749,7 +749,7 @@
    9.40    names than the existing @{typ "'a list"} that is already in @{theory
    9.41    Main}: *}
    9.42  
    9.43 -datatype_new 'a seq = Empty | Seq 'a "'a seq"
    9.44 +datatype 'a seq = Empty | Seq 'a "'a seq"
    9.45  
    9.46  text {* We can now prove some simple lemma by structural induction: *}
    9.47  
    9.48 @@ -1158,9 +1158,9 @@
    9.49    by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject)
    9.50  
    9.51  text {* Note that such trivial constructions are better done with
    9.52 -  derived specification mechanisms such as @{command datatype_new}: *}
    9.53 -
    9.54 -datatype_new three' = One' | Two' | Three'
    9.55 +  derived specification mechanisms such as @{command datatype}: *}
    9.56 +
    9.57 +datatype three' = One' | Two' | Three'
    9.58  
    9.59  text {* This avoids re-doing basic definitions and proofs from the
    9.60    primitive @{command typedef} above. *}
    9.61 @@ -2354,7 +2354,7 @@
    9.62    to reason about inductive types.  Rules are selected according to
    9.63    the declarations by the @{attribute cases} and @{attribute induct}
    9.64    attributes, cf.\ \secref{sec:cases-induct}.  The @{command (HOL)
    9.65 -  datatype_new} package already takes care of this.
    9.66 +  datatype} package already takes care of this.
    9.67  
    9.68    These unstructured tactics feature both goal addressing and dynamic
    9.69    instantiation.  Note that named rule cases are \emph{not} provided
    10.1 --- a/src/Doc/Isar_Ref/Synopsis.thy	Thu Sep 11 19:26:59 2014 +0200
    10.2 +++ b/src/Doc/Isar_Ref/Synopsis.thy	Thu Sep 11 19:32:36 2014 +0200
    10.3 @@ -1068,7 +1068,7 @@
    10.4    provide suitable derived cases rules.
    10.5  *}
    10.6  
    10.7 -datatype_new foo = Foo | Bar foo
    10.8 +datatype foo = Foo | Bar foo
    10.9  
   10.10  notepad
   10.11  begin
    11.1 --- a/src/HOL/Auth/Event.thy	Thu Sep 11 19:26:59 2014 +0200
    11.2 +++ b/src/HOL/Auth/Event.thy	Thu Sep 11 19:32:36 2014 +0200
    11.3 @@ -15,7 +15,7 @@
    11.4  consts  (*Initial states of agents -- parameter of the construction*)
    11.5    initState :: "agent => msg set"
    11.6  
    11.7 -datatype_new
    11.8 +datatype
    11.9    event = Says  agent agent msg
   11.10          | Gets  agent       msg
   11.11          | Notes agent       msg
    12.1 --- a/src/HOL/Auth/Message.thy	Thu Sep 11 19:26:59 2014 +0200
    12.2 +++ b/src/HOL/Auth/Message.thy	Thu Sep 11 19:32:36 2014 +0200
    12.3 @@ -35,10 +35,10 @@
    12.4  definition symKeys :: "key set" where
    12.5    "symKeys == {K. invKey K = K}"
    12.6  
    12.7 -datatype_new  --{*We allow any number of friendly agents*}
    12.8 +datatype  --{*We allow any number of friendly agents*}
    12.9    agent = Server | Friend nat | Spy
   12.10  
   12.11 -datatype_new
   12.12 +datatype
   12.13       msg = Agent  agent     --{*Agent names*}
   12.14           | Number nat       --{*Ordinary integers, timestamps, ...*}
   12.15           | Nonce  nat       --{*Unguessable nonces*}
    13.1 --- a/src/HOL/Auth/Public.thy	Thu Sep 11 19:26:59 2014 +0200
    13.2 +++ b/src/HOL/Auth/Public.thy	Thu Sep 11 19:32:36 2014 +0200
    13.3 @@ -16,7 +16,7 @@
    13.4  
    13.5  subsection{*Asymmetric Keys*}
    13.6  
    13.7 -datatype_new keymode = Signature | Encryption
    13.8 +datatype keymode = Signature | Encryption
    13.9  
   13.10  consts
   13.11    publicKey :: "[keymode,agent] => key"
    14.1 --- a/src/HOL/Auth/Smartcard/EventSC.thy	Thu Sep 11 19:26:59 2014 +0200
    14.2 +++ b/src/HOL/Auth/Smartcard/EventSC.thy	Thu Sep 11 19:32:36 2014 +0200
    14.3 @@ -9,10 +9,10 @@
    14.4  consts  (*Initial states of agents -- parameter of the construction*)
    14.5    initState :: "agent => msg set"
    14.6  
    14.7 -datatype_new card = Card agent
    14.8 +datatype card = Card agent
    14.9  
   14.10  text{*Four new events express the traffic between an agent and his card*}
   14.11 -datatype_new  
   14.12 +datatype  
   14.13    event = Says  agent agent msg
   14.14          | Notes agent       msg
   14.15          | Gets  agent       msg
    15.1 --- a/src/HOL/Auth/TLS.thy	Thu Sep 11 19:26:59 2014 +0200
    15.2 +++ b/src/HOL/Auth/TLS.thy	Thu Sep 11 19:32:36 2014 +0200
    15.3 @@ -49,7 +49,7 @@
    15.4  signature.  Therefore, we formalize signature as encryption using the
    15.5  private encryption key.*}
    15.6  
    15.7 -datatype_new role = ClientRole | ServerRole
    15.8 +datatype role = ClientRole | ServerRole
    15.9  
   15.10  consts
   15.11    (*Pseudo-random function of Section 5*)
    16.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 11 19:26:59 2014 +0200
    16.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 11 19:32:36 2014 +0200
    16.3 @@ -13,7 +13,7 @@
    16.4  imports BNF_Fixpoint_Base
    16.5  keywords
    16.6    "datatype" :: thy_decl and
    16.7 -  "datatype_new" :: thy_decl and
    16.8 +  "datatype" :: thy_decl and
    16.9    "datatype_compat" :: thy_decl
   16.10  begin
   16.11  
    17.1 --- a/src/HOL/Bali/AxSem.thy	Thu Sep 11 19:26:59 2014 +0200
    17.2 +++ b/src/HOL/Bali/AxSem.thy	Thu Sep 11 19:32:36 2014 +0200
    17.3 @@ -378,7 +378,7 @@
    17.4                               \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
    17.5                 \<and> s\<Colon>\<preceq>(G,L))"
    17.6  
    17.7 -datatype_new    'a triple = triple "('a assn)" "term" "('a assn)" (** should be
    17.8 +datatype    'a triple = triple "('a assn)" "term" "('a assn)" (** should be
    17.9  something like triple = \<forall>'a. triple ('a assn) term ('a assn)   **)
   17.10                                          ("{(1_)}/ _>/ {(1_)}"      [3,65,3]75)
   17.11  type_synonym 'a triples = "'a triple set"
    18.1 --- a/src/HOL/Bali/Basis.thy	Thu Sep 11 19:26:59 2014 +0200
    18.2 +++ b/src/HOL/Bali/Basis.thy	Thu Sep 11 19:32:36 2014 +0200
    18.3 @@ -155,7 +155,7 @@
    18.4  primrec the_Inr :: "'a + 'b \<Rightarrow> 'b"
    18.5    where "the_Inr (Inr b) = b"
    18.6  
    18.7 -datatype_new ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
    18.8 +datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
    18.9  
   18.10  primrec the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
   18.11    where "the_In1 (In1 a) = a"
    19.1 --- a/src/HOL/Bali/Decl.thy	Thu Sep 11 19:26:59 2014 +0200
    19.2 +++ b/src/HOL/Bali/Decl.thy	Thu Sep 11 19:32:36 2014 +0200
    19.3 @@ -42,7 +42,7 @@
    19.4  
    19.5  subsubsection {* Access modifier *}
    19.6  
    19.7 -datatype_new acc_modi (* access modifier *)
    19.8 +datatype acc_modi (* access modifier *)
    19.9           = Private | Package | Protected | Public 
   19.10  
   19.11  text {* 
   19.12 @@ -223,9 +223,9 @@
   19.13  introduce the notion of a member declaration (e.g. useful to define 
   19.14  accessiblity ) *}
   19.15  
   19.16 -datatype_new memberdecl = fdecl fdecl | mdecl mdecl
   19.17 +datatype memberdecl = fdecl fdecl | mdecl mdecl
   19.18  
   19.19 -datatype_new memberid = fid vname | mid sig
   19.20 +datatype memberid = fid vname | mid sig
   19.21  
   19.22  class has_memberid =
   19.23    fixes memberid :: "'a \<Rightarrow> memberid"
    20.1 --- a/src/HOL/Bali/Example.thy	Thu Sep 11 19:26:59 2014 +0200
    20.2 +++ b/src/HOL/Bali/Example.thy	Thu Sep 11 19:32:36 2014 +0200
    20.3 @@ -66,9 +66,9 @@
    20.4  section "type and expression names"
    20.5  
    20.6  (** unfortunately cannot simply instantiate tnam **)
    20.7 -datatype_new tnam'  = HasFoo' | Base' | Ext' | Main'
    20.8 -datatype_new vnam'  = arr' | vee' | z' | e'
    20.9 -datatype_new label' = lab1'
   20.10 +datatype tnam'  = HasFoo' | Base' | Ext' | Main'
   20.11 +datatype vnam'  = arr' | vee' | z' | e'
   20.12 +datatype label' = lab1'
   20.13  
   20.14  axiomatization
   20.15    tnam' :: "tnam'  \<Rightarrow> tnam" and
    21.1 --- a/src/HOL/Bali/Name.thy	Thu Sep 11 19:26:59 2014 +0200
    21.2 +++ b/src/HOL/Bali/Name.thy	Thu Sep 11 19:32:36 2014 +0200
    21.3 @@ -12,11 +12,11 @@
    21.4  typedecl vname  --{* variable or field name *}
    21.5  typedecl label  --{* label as destination of break or continue *}
    21.6  
    21.7 -datatype_new ename        --{* expression name *} 
    21.8 +datatype ename        --{* expression name *} 
    21.9          = VNam vname 
   21.10          | Res         --{* special name to model the return value of methods *}
   21.11  
   21.12 -datatype_new lname        --{* names for local variables and the This pointer *}
   21.13 +datatype lname        --{* names for local variables and the This pointer *}
   21.14          = EName ename 
   21.15          | This
   21.16  abbreviation VName   :: "vname \<Rightarrow> lname"
   21.17 @@ -25,7 +25,7 @@
   21.18  abbreviation Result :: lname
   21.19        where "Result == EName Res"
   21.20  
   21.21 -datatype_new xname          --{* names of standard exceptions *}
   21.22 +datatype xname          --{* names of standard exceptions *}
   21.23          = Throwable
   21.24          | NullPointer | OutOfMemory | ClassCast   
   21.25          | NegArrSize  | IndOutBound | ArrStore
   21.26 @@ -39,7 +39,7 @@
   21.27  done
   21.28  
   21.29  
   21.30 -datatype_new tname  --{* type names for standard classes and other type names *}
   21.31 +datatype tname  --{* type names for standard classes and other type names *}
   21.32          = Object'
   21.33          | SXcpt'   xname
   21.34          | TName   tnam
    22.1 --- a/src/HOL/Bali/State.thy	Thu Sep 11 19:26:59 2014 +0200
    22.2 +++ b/src/HOL/Bali/State.thy	Thu Sep 11 19:32:36 2014 +0200
    22.3 @@ -19,7 +19,7 @@
    22.4  
    22.5  section "objects"
    22.6  
    22.7 -datatype_new  obj_tag =     --{* tag for generic object   *}
    22.8 +datatype  obj_tag =     --{* tag for generic object   *}
    22.9            CInst qtname  --{* class instance           *}
   22.10          | Arr  ty int   --{* array with component type and length *}
   22.11      --{* | CStat qtname   the tag is irrelevant for a class object,
   22.12 @@ -225,7 +225,7 @@
   22.13   (type) "heap"   <= (type) "(loc  , obj) table"
   22.14  (*  (type) "locals" <= (type) "(lname, val) table" *)
   22.15  
   22.16 -datatype_new st = (* pure state, i.e. contents of all variables *)
   22.17 +datatype st = (* pure state, i.e. contents of all variables *)
   22.18           st globs locals
   22.19  
   22.20  subsection "access"
    23.1 --- a/src/HOL/Bali/Term.thy	Thu Sep 11 19:26:59 2014 +0200
    23.2 +++ b/src/HOL/Bali/Term.thy	Thu Sep 11 19:32:36 2014 +0200
    23.3 @@ -60,20 +60,20 @@
    23.4  type_synonym locals = "(lname, val) table"  --{* local variables *}
    23.5  
    23.6  
    23.7 -datatype_new jump
    23.8 +datatype jump
    23.9          = Break label --{* break *}
   23.10          | Cont label  --{* continue *}
   23.11          | Ret         --{* return from method *}
   23.12  
   23.13 -datatype_new xcpt        --{* exception *}
   23.14 +datatype xcpt        --{* exception *}
   23.15          = Loc loc    --{* location of allocated execption object *}
   23.16          | Std xname  --{* intermediate standard exception, see Eval.thy *}
   23.17  
   23.18 -datatype_new error
   23.19 +datatype error
   23.20         =  AccessViolation  --{* Access to a member that isn't permitted *}
   23.21          | CrossMethodJump  --{* Method exits with a break or continue *}
   23.22  
   23.23 -datatype_new abrupt       --{* abrupt completion *} 
   23.24 +datatype abrupt       --{* abrupt completion *} 
   23.25          = Xcpt xcpt   --{* exception *}
   23.26          | Jump jump   --{* break, continue, return *}
   23.27          | Error error -- {* runtime errors, we wan't to detect and proof absent
   23.28 @@ -90,7 +90,7 @@
   23.29  translations
   23.30   (type) "locals" <= (type) "(lname, val) table"
   23.31  
   23.32 -datatype_new inv_mode                  --{* invocation mode for method calls *}
   23.33 +datatype inv_mode                  --{* invocation mode for method calls *}
   23.34          = Static                   --{* static *}
   23.35          | SuperM                   --{* super  *}
   23.36          | IntVir                   --{* interface or virtual *}
   23.37 @@ -104,13 +104,13 @@
   23.38    (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
   23.39  
   23.40  --{* function codes for unary operations *}
   23.41 -datatype_new unop =  UPlus    -- {*{\tt +} unary plus*} 
   23.42 +datatype unop =  UPlus    -- {*{\tt +} unary plus*} 
   23.43                 | UMinus   -- {*{\tt -} unary minus*}
   23.44                 | UBitNot  -- {*{\tt ~} bitwise NOT*}
   23.45                 | UNot     -- {*{\tt !} logical complement*}
   23.46  
   23.47  --{* function codes for binary operations *}
   23.48 -datatype_new binop = Mul     -- {*{\tt * }   multiplication*}
   23.49 +datatype binop = Mul     -- {*{\tt * }   multiplication*}
   23.50                 | Div     -- {*{\tt /}   division*}
   23.51                 | Mod     -- {*{\tt \%}   remainder*}
   23.52                 | Plus    -- {*{\tt +}   addition*}
   23.53 @@ -140,7 +140,7 @@
   23.54        {\tt true || e} e is not evaluated; 
   23.55  *}
   23.56  
   23.57 -datatype_new var
   23.58 +datatype var
   23.59          = LVar lname --{* local variable (incl. parameters) *}
   23.60          | FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90)
   23.61                       --{* class field *}
    24.1 --- a/src/HOL/Bali/Type.thy	Thu Sep 11 19:26:59 2014 +0200
    24.2 +++ b/src/HOL/Bali/Type.thy	Thu Sep 11 19:32:36 2014 +0200
    24.3 @@ -14,13 +14,13 @@
    24.4  \end{itemize}
    24.5  *}
    24.6  
    24.7 -datatype_new prim_ty        --{* primitive type, cf. 4.2 *}
    24.8 +datatype prim_ty        --{* primitive type, cf. 4.2 *}
    24.9          = Void          --{* result type of void methods *}
   24.10          | Boolean
   24.11          | Integer
   24.12  
   24.13  
   24.14 -datatype_new ref_ty         --{* reference type, cf. 4.3 *}
   24.15 +datatype ref_ty         --{* reference type, cf. 4.3 *}
   24.16          = NullT         --{* null type, cf. 4.1 *}
   24.17          | IfaceT qtname --{* interface type *}
   24.18          | ClassT qtname --{* class type *}
    25.1 --- a/src/HOL/Bali/Value.thy	Thu Sep 11 19:26:59 2014 +0200
    25.2 +++ b/src/HOL/Bali/Value.thy	Thu Sep 11 19:32:36 2014 +0200
    25.3 @@ -9,7 +9,7 @@
    25.4  
    25.5  typedecl loc            --{* locations, i.e. abstract references on objects *}
    25.6  
    25.7 -datatype_new val
    25.8 +datatype val
    25.9          = Unit          --{* dummy result value of void methods *}
   25.10          | Bool bool     --{* Boolean value *}
   25.11          | Intg int      --{* integer value *}
    26.1 --- a/src/HOL/Code_Evaluation.thy	Thu Sep 11 19:26:59 2014 +0200
    26.2 +++ b/src/HOL/Code_Evaluation.thy	Thu Sep 11 19:32:36 2014 +0200
    26.3 @@ -13,7 +13,7 @@
    26.4  
    26.5  subsubsection {* Terms and class @{text term_of} *}
    26.6  
    26.7 -datatype_new "term" = dummy_term
    26.8 +datatype "term" = dummy_term
    26.9  
   26.10  definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
   26.11    "Const _ _ = dummy_term"
    27.1 --- a/src/HOL/Codegenerator_Test/Code_Test.thy	Thu Sep 11 19:26:59 2014 +0200
    27.2 +++ b/src/HOL/Codegenerator_Test/Code_Test.thy	Thu Sep 11 19:32:36 2014 +0200
    27.3 @@ -11,7 +11,7 @@
    27.4  
    27.5  subsection {* YXML encoding for @{typ Code_Evaluation.term} *}
    27.6  
    27.7 -datatype_new yxml_of_term = YXML
    27.8 +datatype yxml_of_term = YXML
    27.9  
   27.10  lemma yot_anything: "x = (y :: yxml_of_term)"
   27.11  by(cases x y rule: yxml_of_term.exhaust[case_product yxml_of_term.exhaust])(simp)
   27.12 @@ -58,7 +58,7 @@
   27.13    sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}.
   27.14  *}
   27.15  
   27.16 -datatype_new xml_tree = XML_Tree
   27.17 +datatype xml_tree = XML_Tree
   27.18  
   27.19  lemma xml_tree_anything: "x = (y :: xml_tree)"
   27.20  by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)
    28.1 --- a/src/HOL/Datatype_Examples/Compat.thy	Thu Sep 11 19:26:59 2014 +0200
    28.2 +++ b/src/HOL/Datatype_Examples/Compat.thy	Thu Sep 11 19:32:36 2014 +0200
    28.3 @@ -31,7 +31,7 @@
    28.4  
    28.5  ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name old_lst}; \<close>
    28.6  
    28.7 -datatype_new 'a lst = Nl | Cns 'a "'a lst"
    28.8 +datatype 'a lst = Nl | Cns 'a "'a lst"
    28.9  
   28.10  ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name lst}; \<close>
   28.11  
   28.12 @@ -39,7 +39,7 @@
   28.13  
   28.14  ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name lst}; \<close>
   28.15  
   28.16 -datatype_new 'b w = W | W' "'b w \<times> 'b list"
   28.17 +datatype 'b w = W | W' "'b w \<times> 'b list"
   28.18  
   28.19  (* no support for sums of products:
   28.20  datatype_compat w
   28.21 @@ -47,11 +47,11 @@
   28.22  
   28.23  ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name w}; \<close>
   28.24  
   28.25 -datatype_new ('c, 'b) s = L 'c | R 'b
   28.26 +datatype ('c, 'b) s = L 'c | R 'b
   28.27  
   28.28  ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name s}; \<close>
   28.29  
   28.30 -datatype_new 'd x = X | X' "('d x lst, 'd list) s"
   28.31 +datatype 'd x = X | X' "('d x lst, 'd list) s"
   28.32  
   28.33  ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name x}; \<close>
   28.34  
   28.35 @@ -67,7 +67,7 @@
   28.36  thm x.induct x.rec
   28.37  thm compat_x.induct compat_x.rec
   28.38  
   28.39 -datatype_new 'a tttre = TTTre 'a "'a tttre lst lst lst"
   28.40 +datatype 'a tttre = TTTre 'a "'a tttre lst lst lst"
   28.41  
   28.42  ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tttre}; \<close>
   28.43  
   28.44 @@ -78,7 +78,7 @@
   28.45  thm tttre.induct tttre.rec
   28.46  thm compat_tttre.induct compat_tttre.rec
   28.47  
   28.48 -datatype_new 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst"
   28.49 +datatype 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst"
   28.50  
   28.51  ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name ftre}; \<close>
   28.52  
   28.53 @@ -89,7 +89,7 @@
   28.54  thm ftre.induct ftre.rec
   28.55  thm compat_ftre.induct compat_ftre.rec
   28.56  
   28.57 -datatype_new 'a btre = BTre 'a "'a btre lst" "'a btre lst"
   28.58 +datatype 'a btre = BTre 'a "'a btre lst" "'a btre lst"
   28.59  
   28.60  ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name btre}; \<close>
   28.61  
   28.62 @@ -100,7 +100,7 @@
   28.63  thm btre.induct btre.rec
   28.64  thm compat_btre.induct compat_btre.rec
   28.65  
   28.66 -datatype_new 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo"
   28.67 +datatype 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo"
   28.68  
   28.69  ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo}; \<close>
   28.70  ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar}; \<close>
   28.71 @@ -110,7 +110,7 @@
   28.72  ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo}; \<close>
   28.73  ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar}; \<close>
   28.74  
   28.75 -datatype_new 'a tre = Tre 'a "'a tre lst"
   28.76 +datatype 'a tre = Tre 'a "'a tre lst"
   28.77  
   28.78  ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tre}; \<close>
   28.79  
   28.80 @@ -121,12 +121,12 @@
   28.81  thm tre.induct tre.rec
   28.82  thm compat_tre.induct compat_tre.rec
   28.83  
   28.84 -datatype_new 'a f = F 'a and 'a g = G 'a
   28.85 +datatype 'a f = F 'a and 'a g = G 'a
   28.86  
   28.87  ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name f}; \<close>
   28.88  ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name g}; \<close>
   28.89  
   28.90 -datatype_new h = H "h f" | H'
   28.91 +datatype h = H "h f" | H'
   28.92  
   28.93  ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name h}; \<close>
   28.94  
   28.95 @@ -143,7 +143,7 @@
   28.96  thm h.induct h.rec
   28.97  thm compat_h.induct compat_h.rec
   28.98  
   28.99 -datatype_new myunit = MyUnity
  28.100 +datatype myunit = MyUnity
  28.101  
  28.102  ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name myunit}; \<close>
  28.103  
  28.104 @@ -151,7 +151,7 @@
  28.105  
  28.106  ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name myunit}; \<close>
  28.107  
  28.108 -datatype_new mylist = MyNil | MyCons nat mylist
  28.109 +datatype mylist = MyNil | MyCons nat mylist
  28.110  
  28.111  ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name mylist}; \<close>
  28.112  
  28.113 @@ -159,7 +159,7 @@
  28.114  
  28.115  ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name mylist}; \<close>
  28.116  
  28.117 -datatype_new foo' = FooNil | FooCons bar' foo' and bar' = Bar
  28.118 +datatype foo' = FooNil | FooCons bar' foo' and bar' = Bar
  28.119  
  28.120  ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo'}; \<close>
  28.121  ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar'}; \<close>
  28.122 @@ -177,7 +177,7 @@
  28.123  
  28.124  ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name fnky}; \<close>
  28.125  
  28.126 -datatype_new tree = Tree "tree foo"
  28.127 +datatype tree = Tree "tree foo"
  28.128  
  28.129  ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tree}; \<close>
  28.130  
    29.1 --- a/src/HOL/Datatype_Examples/IsaFoR_Datatypes.thy	Thu Sep 11 19:26:59 2014 +0200
    29.2 +++ b/src/HOL/Datatype_Examples/IsaFoR_Datatypes.thy	Thu Sep 11 19:32:36 2014 +0200
    29.3 @@ -11,16 +11,16 @@
    29.4  imports Real
    29.5  begin
    29.6  
    29.7 -datatype_new (discs_sels) ('f, 'l) lab =
    29.8 +datatype (discs_sels) ('f, 'l) lab =
    29.9      Lab "('f, 'l) lab" 'l
   29.10    | FunLab "('f, 'l) lab" "('f, 'l) lab list"
   29.11    | UnLab 'f
   29.12    | Sharp "('f, 'l) lab"
   29.13  
   29.14 -datatype_new (discs_sels) 'f projL = Projection "(('f \<times> nat) \<times> nat) list"
   29.15 +datatype (discs_sels) 'f projL = Projection "(('f \<times> nat) \<times> nat) list"
   29.16  
   29.17 -datatype_new (discs_sels) ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
   29.18 -datatype_new (discs_sels) ('f, 'v) ctxt =
   29.19 +datatype (discs_sels) ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
   29.20 +datatype (discs_sels) ('f, 'v) ctxt =
   29.21      Hole ("\<box>")
   29.22    | More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list"
   29.23  
   29.24 @@ -32,7 +32,7 @@
   29.25  type_synonym ('f, 'l, 'v) trsLL   = "(('f, 'l) lab, 'v) rules"
   29.26  type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list"
   29.27  
   29.28 -datatype_new (discs_sels) pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70)
   29.29 +datatype (discs_sels) pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70)
   29.30  
   29.31  type_synonym  ('f, 'v) prseq = "(pos \<times> ('f, 'v) rule \<times> bool \<times> ('f, 'v) term) list"
   29.32  type_synonym  ('f, 'v) rseq = "(pos \<times> ('f, 'v) rule \<times> ('f, 'v) term) list"
   29.33 @@ -49,7 +49,7 @@
   29.34  type_synonym ('f, 'l, 'v) qtrsLL =
   29.35    "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL"
   29.36  
   29.37 -datatype_new (discs_sels) location = H | A | B | R
   29.38 +datatype (discs_sels) location = H | A | B | R
   29.39  
   29.40  type_synonym ('f, 'v) forb_pattern = "('f, 'v) ctxt \<times> ('f, 'v) term \<times> location"
   29.41  type_synonym ('f, 'v) forb_patterns = "('f, 'v) forb_pattern set"
   29.42 @@ -68,20 +68,20 @@
   29.43  type_synonym 'a vec = "'a list"
   29.44  type_synonym 'a mat = "'a vec list"
   29.45  
   29.46 -datatype_new (discs_sels) arctic = MinInfty | Num_arc int
   29.47 -datatype_new (discs_sels) 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
   29.48 -datatype_new (discs_sels) order_tag = Lex | Mul
   29.49 +datatype (discs_sels) arctic = MinInfty | Num_arc int
   29.50 +datatype (discs_sels) 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
   29.51 +datatype (discs_sels) order_tag = Lex | Mul
   29.52  
   29.53  type_synonym 'f status_prec_repr = "(('f \<times> nat) \<times> (nat \<times> order_tag)) list"
   29.54  
   29.55 -datatype_new (discs_sels) af_entry =
   29.56 +datatype (discs_sels) af_entry =
   29.57      Collapse nat
   29.58    | AFList "nat list"
   29.59  
   29.60  type_synonym 'f afs_list = "(('f \<times> nat) \<times> af_entry) list"
   29.61  type_synonym 'f prec_weight_repr = "(('f \<times> nat) \<times> (nat \<times> nat \<times> (nat list option))) list \<times> nat"
   29.62  
   29.63 -datatype_new (discs_sels) 'f redtriple_impl =
   29.64 +datatype (discs_sels) 'f redtriple_impl =
   29.65      Int_carrier "('f, int) lpoly_interL"
   29.66    | Int_nl_carrier "('f, int) poly_inter_list"
   29.67    | Rat_carrier "('f, rat) lpoly_interL"
   29.68 @@ -98,15 +98,15 @@
   29.69    | RPO "'f status_prec_repr" "'f afs_list"
   29.70    | KBO "'f prec_weight_repr" "'f afs_list"
   29.71  
   29.72 -datatype_new (discs_sels) list_order_type = MS_Ext | Max_Ext | Min_Ext  | Dms_Ext
   29.73 +datatype (discs_sels) list_order_type = MS_Ext | Max_Ext | Min_Ext  | Dms_Ext
   29.74  type_synonym 'f scnp_af = "(('f \<times> nat) \<times> (nat \<times> nat) list) list"
   29.75  
   29.76 -datatype_new (discs_sels) 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"
   29.77 +datatype (discs_sels) 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"
   29.78  
   29.79  type_synonym 'f sig_map_list = "(('f \<times> nat) \<times> 'f list) list"
   29.80  type_synonym ('f, 'v) uncurry_info = "'f \<times> 'f sig_map_list \<times> ('f, 'v) rules \<times> ('f, 'v) rules"
   29.81  
   29.82 -datatype_new (discs_sels) arithFun =
   29.83 +datatype (discs_sels) arithFun =
   29.84      Arg nat
   29.85    | Const nat
   29.86    | Sum "arithFun list"
   29.87 @@ -115,25 +115,25 @@
   29.88    | Prod "arithFun list"
   29.89    | IfEqual arithFun arithFun arithFun arithFun
   29.90  
   29.91 -datatype_new (discs_sels) 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list"
   29.92 -datatype_new (discs_sels) ('f, 'v) sl_variant =
   29.93 +datatype (discs_sels) 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list"
   29.94 +datatype (discs_sels) ('f, 'v) sl_variant =
   29.95      Rootlab "('f \<times> nat) option"
   29.96    | Finitelab "'f sl_inter"
   29.97    | QuasiFinitelab "'f sl_inter" 'v
   29.98  
   29.99  type_synonym ('f, 'v) crit_pair_joins = "(('f, 'v) term \<times> ('f, 'v) rseq \<times> ('f, 'v) term \<times> ('f, 'v) rseq) list"
  29.100  
  29.101 -datatype_new (discs_sels) 'f join_info = Guided "('f, string) crit_pair_joins" | Join_NF | Join_BFS nat
  29.102 +datatype (discs_sels) 'f join_info = Guided "('f, string) crit_pair_joins" | Join_NF | Join_BFS nat
  29.103  
  29.104  type_synonym unknown_info = string
  29.105  
  29.106  type_synonym dummy_prf = unit
  29.107  
  29.108 -datatype_new (discs_sels) ('f, 'v) complex_constant_removal_prf = Complex_Constant_Removal_Proof
  29.109 +datatype (discs_sels) ('f, 'v) complex_constant_removal_prf = Complex_Constant_Removal_Proof
  29.110    "('f, 'v) term"
  29.111    "(('f, 'v) rule \<times> ('f, 'v) rule) list"
  29.112  
  29.113 -datatype_new (discs_sels) ('f, 'v) cond_constraint =
  29.114 +datatype (discs_sels) ('f, 'v) cond_constraint =
  29.115      CC_cond bool "('f, 'v) rule"
  29.116    | CC_rewr "('f, 'v) term" "('f, 'v) term"
  29.117    | CC_impl "('f, 'v) cond_constraint list" "('f, 'v) cond_constraint"
  29.118 @@ -142,7 +142,7 @@
  29.119  type_synonym ('f, 'v, 'w) gsubstL = "('v \<times> ('f, 'w) term) list"
  29.120  type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL"
  29.121  
  29.122 -datatype_new (discs_sels) ('f, 'v) cond_constraint_prf =
  29.123 +datatype (discs_sels) ('f, 'v) cond_constraint_prf =
  29.124      Final
  29.125    | Delete_Condition "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
  29.126    | Different_Constructor "('f, 'v) cond_constraint"
  29.127 @@ -152,28 +152,28 @@
  29.128    | Simplify_Condition "('f, 'v) cond_constraint" "('f, 'v) substL" "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
  29.129    | Induction "('f, 'v) cond_constraint" "('f, 'v) cond_constraint list" "(('f, 'v) rule \<times> (('f, 'v) term \<times> 'v list) list \<times> ('f, 'v) cond_constraint \<times> ('f, 'v) cond_constraint_prf) list"
  29.130  
  29.131 -datatype_new (discs_sels) ('f, 'v) cond_red_pair_prf =
  29.132 +datatype (discs_sels) ('f, 'v) cond_red_pair_prf =
  29.133    Cond_Red_Pair_Prf
  29.134      'f "(('f, 'v) cond_constraint \<times> ('f, 'v) rules \<times> ('f, 'v) cond_constraint_prf) list" nat nat
  29.135  
  29.136 -datatype_new (discs_sels) ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
  29.137 -datatype_new (discs_sels) ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \<times> 'q) list"
  29.138 -datatype_new (discs_sels) 'q ta_relation =
  29.139 +datatype (discs_sels) ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
  29.140 +datatype (discs_sels) ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \<times> 'q) list"
  29.141 +datatype (discs_sels) 'q ta_relation =
  29.142      Decision_Proc
  29.143    | Id_Relation
  29.144    | Some_Relation "('q \<times> 'q) list"
  29.145  
  29.146 -datatype_new (discs_sels) boundstype = Roof | Match
  29.147 -datatype_new (discs_sels) ('f, 'q) bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
  29.148 +datatype (discs_sels) boundstype = Roof | Match
  29.149 +datatype (discs_sels) ('f, 'q) bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
  29.150  
  29.151 -datatype_new (discs_sels) ('f, 'v) pat_eqv_prf =
  29.152 +datatype (discs_sels) ('f, 'v) pat_eqv_prf =
  29.153      Pat_Dom_Renaming "('f, 'v) substL"
  29.154    | Pat_Irrelevant "('f, 'v) substL" "('f, 'v) substL"
  29.155    | Pat_Simplify "('f, 'v) substL" "('f, 'v) substL"
  29.156  
  29.157 -datatype_new (discs_sels) pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close
  29.158 +datatype (discs_sels) pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close
  29.159  
  29.160 -datatype_new (discs_sels) ('f, 'v) pat_rule_prf =
  29.161 +datatype (discs_sels) ('f, 'v) pat_rule_prf =
  29.162      Pat_OrigRule "('f, 'v) rule" bool
  29.163    | Pat_InitPump "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL"
  29.164    | Pat_InitPumpCtxt "('f, 'v) pat_rule_prf" "('f, 'v) substL" pos 'v
  29.165 @@ -183,10 +183,10 @@
  29.166    | Pat_Rewr "('f, 'v) pat_rule_prf" "('f, 'v) term \<times> ('f, 'v) rseq" pat_rule_pos 'v
  29.167    | Pat_Exp_Sigma "('f, 'v) pat_rule_prf" nat
  29.168  
  29.169 -datatype_new (discs_sels) ('f, 'v) non_loop_prf =
  29.170 +datatype (discs_sels) ('f, 'v) non_loop_prf =
  29.171      Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos
  29.172  
  29.173 -datatype_new (discs_sels) ('f, 'l, 'v) problem =
  29.174 +datatype (discs_sels) ('f, 'l, 'v) problem =
  29.175      SN_TRS "('f, 'l, 'v) qreltrsLL"
  29.176    | SN_FP_TRS "('f, 'l, 'v) fptrsLL"
  29.177    | Finite_DPP "('f, 'l, 'v) dppLL"
  29.178 @@ -198,7 +198,7 @@
  29.179  
  29.180  declare [[bnf_timing]]
  29.181  
  29.182 -datatype_new (discs_sels) ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof =
  29.183 +datatype (discs_sels) ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof =
  29.184      SN_assm_proof "('f, 'l, 'v) qreltrsLL" 'a
  29.185    | Finite_assm_proof "('f, 'l, 'v) dppLL" 'b
  29.186    | SN_FP_assm_proof "('f, 'l, 'v) fptrsLL" 'c
  29.187 @@ -210,7 +210,7 @@
  29.188  
  29.189  type_synonym ('f, 'l, 'v, 'a, 'b, 'c, 'd) assm_proof = "('f, 'l, 'v, 'a, 'b, 'c, dummy_prf, 'd) generic_assm_proof"
  29.190  
  29.191 -datatype_new (discs_sels) ('f, 'l, 'v) assm =
  29.192 +datatype (discs_sels) ('f, 'l, 'v) assm =
  29.193      SN_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) qreltrsLL"
  29.194    | SN_FP_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) fptrsLL"
  29.195    | Finite_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) dppLL"
  29.196 @@ -254,7 +254,7 @@
  29.197  | "collect_neg_assms tp dpp rtp fptp unk (Unknown_assm_proof p prf) = unk prf"
  29.198  | "collect_neg_assms tp dpp rtp fptp unk _ = []"
  29.199  
  29.200 -datatype_new (discs_sels) ('f, 'l, 'v) dp_nontermination_proof =
  29.201 +datatype (discs_sels) ('f, 'l, 'v) dp_nontermination_proof =
  29.202      DP_Loop "(('f, 'l) lab, 'v) term" "(('f, 'l) lab, 'v) prseq" "(('f, 'l) lab, 'v) substL" "(('f, 'l) lab, 'v) ctxt"
  29.203    | DP_Nonloop "(('f, 'l) lab, 'v) non_loop_prf"
  29.204    | DP_Rule_Removal "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_nontermination_proof"
  29.205 @@ -312,7 +312,7 @@
  29.206         ('f, 'l, 'v) fp_nontermination_proof,
  29.207         ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
  29.208  
  29.209 -datatype_new (discs_sels) ('f, 'l, 'v) dp_termination_proof =
  29.210 +datatype (discs_sels) ('f, 'l, 'v) dp_termination_proof =
  29.211      P_is_Empty
  29.212    | Subterm_Criterion_Proc "('f, 'l) lab projL" "('f, 'l, 'v) rseqL"
  29.213        "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
    30.1 --- a/src/HOL/Datatype_Examples/Lambda_Term.thy	Thu Sep 11 19:26:59 2014 +0200
    30.2 +++ b/src/HOL/Datatype_Examples/Lambda_Term.thy	Thu Sep 11 19:32:36 2014 +0200
    30.3 @@ -14,7 +14,7 @@
    30.4  
    30.5  section {* Datatype definition *}
    30.6  
    30.7 -datatype_new 'a trm =
    30.8 +datatype 'a trm =
    30.9    Var 'a |
   30.10    App "'a trm" "'a trm" |
   30.11    Lam 'a "'a trm" |
    31.1 --- a/src/HOL/Datatype_Examples/Misc_Datatype.thy	Thu Sep 11 19:26:59 2014 +0200
    31.2 +++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy	Thu Sep 11 19:32:36 2014 +0200
    31.3 @@ -13,26 +13,26 @@
    31.4  imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/FSet"
    31.5  begin
    31.6  
    31.7 -datatype_new (discs_sels) simple = X1 | X2 | X3 | X4
    31.8 +datatype (discs_sels) simple = X1 | X2 | X3 | X4
    31.9  
   31.10 -datatype_new (discs_sels) simple' = X1' unit | X2' unit | X3' unit | X4' unit
   31.11 +datatype (discs_sels) simple' = X1' unit | X2' unit | X3' unit | X4' unit
   31.12  
   31.13 -datatype_new (discs_sels) simple'' = X1'' nat int | X2''
   31.14 +datatype (discs_sels) simple'' = X1'' nat int | X2''
   31.15  
   31.16 -datatype_new (discs_sels) 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
   31.17 +datatype (discs_sels) 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
   31.18  
   31.19 -datatype_new (discs_sels) ('b, 'c :: ord, 'd, 'e) some_passive =
   31.20 +datatype (discs_sels) ('b, 'c :: ord, 'd, 'e) some_passive =
   31.21    SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
   31.22  
   31.23 -datatype_new (discs_sels) hfset = HFset "hfset fset"
   31.24 +datatype (discs_sels) hfset = HFset "hfset fset"
   31.25  
   31.26 -datatype_new (discs_sels) lambda =
   31.27 +datatype (discs_sels) lambda =
   31.28    Var string |
   31.29    App lambda lambda |
   31.30    Abs string lambda |
   31.31    Let "(string \<times> lambda) fset" lambda
   31.32  
   31.33 -datatype_new (discs_sels) 'a par_lambda =
   31.34 +datatype (discs_sels) 'a par_lambda =
   31.35    PVar 'a |
   31.36    PApp "'a par_lambda" "'a par_lambda" |
   31.37    PAbs 'a "'a par_lambda" |
   31.38 @@ -43,70 +43,70 @@
   31.39    ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
   31.40  *)
   31.41  
   31.42 -datatype_new (discs_sels) 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
   31.43 +datatype (discs_sels) 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
   31.44  and 'a I2 = I21 | I22 "'a I1" "'a I2"
   31.45  
   31.46 -datatype_new (discs_sels) 'a tree = TEmpty | TNode 'a "'a forest"
   31.47 +datatype (discs_sels) 'a tree = TEmpty | TNode 'a "'a forest"
   31.48  and 'a forest = FNil | FCons "'a tree" "'a forest"
   31.49  
   31.50 -datatype_new (discs_sels) 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
   31.51 +datatype (discs_sels) 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
   31.52  and 'a branch = Branch 'a "'a tree'"
   31.53  
   31.54 -datatype_new (discs_sels) 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist"
   31.55 +datatype (discs_sels) 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist"
   31.56  
   31.57 -datatype_new (discs_sels) ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
   31.58 +datatype (discs_sels) ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
   31.59  and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
   31.60  and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
   31.61  
   31.62 -datatype_new (discs_sels) 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
   31.63 +datatype (discs_sels) 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
   31.64  
   31.65 -datatype_new (discs_sels) ('a, 'b, 'c) some_killing =
   31.66 +datatype (discs_sels) ('a, 'b, 'c) some_killing =
   31.67    SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
   31.68  and ('a, 'b, 'c) in_here =
   31.69    IH1 'b 'a | IH2 'c
   31.70  
   31.71 -datatype_new (discs_sels) 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b
   31.72 -datatype_new (discs_sels) 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
   31.73 -datatype_new (discs_sels) 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset"
   31.74 -datatype_new (discs_sels) 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list"
   31.75 +datatype (discs_sels) 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b
   31.76 +datatype (discs_sels) 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
   31.77 +datatype (discs_sels) 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset"
   31.78 +datatype (discs_sels) 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list"
   31.79  
   31.80  (*
   31.81 -datatype_new (discs_sels) 'b fail = F "'b fail" 'b "'b fail" "'b list"
   31.82 -datatype_new (discs_sels) 'b fail = F "'b fail" 'b "'b fail" 'b
   31.83 -datatype_new (discs_sels) 'b fail = F1 "'b fail" 'b | F2 "'b fail"
   31.84 -datatype_new (discs_sels) 'b fail = F "'b fail" 'b
   31.85 +datatype (discs_sels) 'b fail = F "'b fail" 'b "'b fail" "'b list"
   31.86 +datatype (discs_sels) 'b fail = F "'b fail" 'b "'b fail" 'b
   31.87 +datatype (discs_sels) 'b fail = F1 "'b fail" 'b | F2 "'b fail"
   31.88 +datatype (discs_sels) 'b fail = F "'b fail" 'b
   31.89  *)
   31.90  
   31.91 -datatype_new (discs_sels) l1 = L1 "l2 list"
   31.92 +datatype (discs_sels) l1 = L1 "l2 list"
   31.93  and l2 = L21 "l1 fset" | L22 l2
   31.94  
   31.95 -datatype_new (discs_sels) kk1 = KK1 kk2
   31.96 +datatype (discs_sels) kk1 = KK1 kk2
   31.97  and kk2 = KK2 kk3
   31.98  and kk3 = KK3 "kk1 list"
   31.99  
  31.100 -datatype_new (discs_sels) t1 = T11 t3 | T12 t2
  31.101 +datatype (discs_sels) t1 = T11 t3 | T12 t2
  31.102  and t2 = T2 t1
  31.103  and t3 = T3
  31.104  
  31.105 -datatype_new (discs_sels) t1' = T11' t2' | T12' t3'
  31.106 +datatype (discs_sels) t1' = T11' t2' | T12' t3'
  31.107  and t2' = T2' t1'
  31.108  and t3' = T3'
  31.109  
  31.110  (*
  31.111 -datatype_new (discs_sels) fail1 = F1 fail2
  31.112 +datatype (discs_sels) fail1 = F1 fail2
  31.113  and fail2 = F2 fail3
  31.114  and fail3 = F3 fail1
  31.115  
  31.116 -datatype_new (discs_sels) fail1 = F1 "fail2 list" fail2
  31.117 +datatype (discs_sels) fail1 = F1 "fail2 list" fail2
  31.118  and fail2 = F2 "fail2 fset" fail3
  31.119  and fail3 = F3 fail1
  31.120  
  31.121 -datatype_new (discs_sels) fail1 = F1 "fail2 list" fail2
  31.122 +datatype (discs_sels) fail1 = F1 "fail2 list" fail2
  31.123  and fail2 = F2 "fail1 fset" fail1
  31.124  *)
  31.125  
  31.126  (* SLOW
  31.127 -datatype_new (discs_sels) ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
  31.128 +datatype (discs_sels) ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
  31.129  and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
  31.130  and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
  31.131  and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list"
  31.132 @@ -117,24 +117,24 @@
  31.133  *)
  31.134  
  31.135  (* fail:
  31.136 -datatype_new (discs_sels) tt1 = TT11 tt2 tt3 | TT12 tt2 tt4
  31.137 +datatype (discs_sels) tt1 = TT11 tt2 tt3 | TT12 tt2 tt4
  31.138  and tt2 = TT2
  31.139  and tt3 = TT3 tt4
  31.140  and tt4 = TT4 tt1
  31.141  *)
  31.142  
  31.143 -datatype_new (discs_sels) k1 = K11 k2 k3 | K12 k2 k4
  31.144 +datatype (discs_sels) k1 = K11 k2 k3 | K12 k2 k4
  31.145  and k2 = K2
  31.146  and k3 = K3 k4
  31.147  and k4 = K4
  31.148  
  31.149 -datatype_new (discs_sels) tt1 = TT11 tt3 tt2 | TT12 tt2 tt4
  31.150 +datatype (discs_sels) tt1 = TT11 tt3 tt2 | TT12 tt2 tt4
  31.151  and tt2 = TT2
  31.152  and tt3 = TT3 tt1
  31.153  and tt4 = TT4
  31.154  
  31.155  (* SLOW
  31.156 -datatype_new (discs_sels) s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2
  31.157 +datatype (discs_sels) s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2
  31.158  and s2 = S21 s7 s5 | S22 s5 s4 s6
  31.159  and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5
  31.160  and s4 = S4 s5
  31.161 @@ -144,35 +144,35 @@
  31.162  and s8 = S8 nat
  31.163  *)
  31.164  
  31.165 -datatype_new (discs_sels) 'a deadbar = DeadBar "'a \<Rightarrow> 'a"
  31.166 -datatype_new (discs_sels) 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
  31.167 -datatype_new (discs_sels) ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
  31.168 -datatype_new (discs_sels) ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
  31.169 -datatype_new (discs_sels) 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a"
  31.170 +datatype (discs_sels) 'a deadbar = DeadBar "'a \<Rightarrow> 'a"
  31.171 +datatype (discs_sels) 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
  31.172 +datatype (discs_sels) ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
  31.173 +datatype (discs_sels) ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
  31.174 +datatype (discs_sels) 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a"
  31.175  
  31.176 -datatype_new (discs_sels) 'a dead_foo = A
  31.177 -datatype_new (discs_sels) ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
  31.178 +datatype (discs_sels) 'a dead_foo = A
  31.179 +datatype (discs_sels) ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
  31.180  
  31.181 -datatype_new (discs_sels) d1 = D
  31.182 -datatype_new (discs_sels) d1' = is_D: D
  31.183 +datatype (discs_sels) d1 = D
  31.184 +datatype (discs_sels) d1' = is_D: D
  31.185  
  31.186 -datatype_new (discs_sels) d2 = D nat
  31.187 -datatype_new (discs_sels) d2' = is_D: D nat
  31.188 +datatype (discs_sels) d2 = D nat
  31.189 +datatype (discs_sels) d2' = is_D: D nat
  31.190  
  31.191 -datatype_new (discs_sels) d3 = D | E
  31.192 -datatype_new (discs_sels) d3' = D | is_E: E
  31.193 -datatype_new (discs_sels) d3'' = is_D: D | E
  31.194 -datatype_new (discs_sels) d3''' = is_D: D | is_E: E
  31.195 +datatype (discs_sels) d3 = D | E
  31.196 +datatype (discs_sels) d3' = D | is_E: E
  31.197 +datatype (discs_sels) d3'' = is_D: D | E
  31.198 +datatype (discs_sels) d3''' = is_D: D | is_E: E
  31.199  
  31.200 -datatype_new (discs_sels) d4 = D nat | E
  31.201 -datatype_new (discs_sels) d4' = D nat | is_E: E
  31.202 -datatype_new (discs_sels) d4'' = is_D: D nat | E
  31.203 -datatype_new (discs_sels) d4''' = is_D: D nat | is_E: E
  31.204 +datatype (discs_sels) d4 = D nat | E
  31.205 +datatype (discs_sels) d4' = D nat | is_E: E
  31.206 +datatype (discs_sels) d4'' = is_D: D nat | E
  31.207 +datatype (discs_sels) d4''' = is_D: D nat | is_E: E
  31.208  
  31.209 -datatype_new (discs_sels) d5 = D nat | E int
  31.210 -datatype_new (discs_sels) d5' = D nat | is_E: E int
  31.211 -datatype_new (discs_sels) d5'' = is_D: D nat | E int
  31.212 -datatype_new (discs_sels) d5''' = is_D: D nat | is_E: E int
  31.213 +datatype (discs_sels) d5 = D nat | E int
  31.214 +datatype (discs_sels) d5' = D nat | is_E: E int
  31.215 +datatype (discs_sels) d5'' = is_D: D nat | E int
  31.216 +datatype (discs_sels) d5''' = is_D: D nat | is_E: E int
  31.217  
  31.218  instance simple :: countable
  31.219    by countable_datatype
    32.1 --- a/src/HOL/Datatype_Examples/Process.thy	Thu Sep 11 19:26:59 2014 +0200
    32.2 +++ b/src/HOL/Datatype_Examples/Process.thy	Thu Sep 11 19:32:36 2014 +0200
    32.3 @@ -79,7 +79,7 @@
    32.4  
    32.5  subsection{* Multi-guard fixpoint definitions, simulated with auxiliary arguments *}
    32.6  
    32.7 -datatype_new x_y_ax = x | y | ax
    32.8 +datatype x_y_ax = x | y | ax
    32.9  
   32.10  primcorec F :: "x_y_ax \<Rightarrow> char list process" where
   32.11    "xyax = x \<Longrightarrow> isChoice (F xyax)"
   32.12 @@ -106,7 +106,7 @@
   32.13  hide_const x y ax X Y AX
   32.14  
   32.15  (* Process terms *)
   32.16 -datatype_new ('a,'pvar) process_term =
   32.17 +datatype ('a,'pvar) process_term =
   32.18   VAR 'pvar |
   32.19   PROC "'a process" |
   32.20   ACT 'a "('a,'pvar) process_term" | CH "('a,'pvar) process_term" "('a,'pvar) process_term"
    33.1 --- a/src/HOL/Datatype_Examples/Stream_Processor.thy	Thu Sep 11 19:26:59 2014 +0200
    33.2 +++ b/src/HOL/Datatype_Examples/Stream_Processor.thy	Thu Sep 11 19:32:36 2014 +0200
    33.3 @@ -14,7 +14,7 @@
    33.4  
    33.5  section {* Continuous Functions on Streams *}
    33.6  
    33.7 -datatype_new ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
    33.8 +datatype ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
    33.9  codatatype ('a, 'b) sp\<^sub>\<nu> = In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
   33.10  
   33.11  primrec run\<^sub>\<mu> :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> ('b \<times> 'c) \<times> 'a stream" where
   33.12 @@ -170,7 +170,7 @@
   33.13  lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_prod \<theta> id o assl"
   33.14    unfolding assl_def \<theta>_def F.map_comp comp_def id_apply convol_def map_prod_def split fst_conv snd_conv ..
   33.15  
   33.16 -datatype_new ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F"
   33.17 +datatype ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F"
   33.18  codatatype ('a, 'b) spF\<^sub>\<nu> = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu>")
   33.19  
   33.20  codatatype 'b JF = Ctor (dtor: "('b, 'b JF) F")
    34.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Sep 11 19:26:59 2014 +0200
    34.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Sep 11 19:32:36 2014 +0200
    34.3 @@ -2037,7 +2037,7 @@
    34.4  
    34.5  subsection "Define syntax and semantics"
    34.6  
    34.7 -datatype_new floatarith
    34.8 +datatype floatarith
    34.9    = Add floatarith floatarith
   34.10    | Minus floatarith
   34.11    | Mult floatarith floatarith
   34.12 @@ -2456,7 +2456,7 @@
   34.13    show ?case by (cases "n < length vs", auto)
   34.14  qed
   34.15  
   34.16 -datatype_new form = Bound floatarith floatarith floatarith form
   34.17 +datatype form = Bound floatarith floatarith floatarith form
   34.18                | Assign floatarith floatarith form
   34.19                | Less floatarith floatarith
   34.20                | LessEqual floatarith floatarith
    35.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Sep 11 19:26:59 2014 +0200
    35.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Sep 11 19:32:36 2014 +0200
    35.3 @@ -11,12 +11,12 @@
    35.4  
    35.5  text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
    35.6  
    35.7 -datatype_new 'a pol =
    35.8 +datatype 'a pol =
    35.9      Pc 'a
   35.10    | Pinj nat "'a pol"
   35.11    | PX "'a pol" nat "'a pol"
   35.12  
   35.13 -datatype_new 'a polex =
   35.14 +datatype 'a polex =
   35.15      Pol "'a pol"
   35.16    | Add "'a polex" "'a polex"
   35.17    | Sub "'a polex" "'a polex"
    36.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Thu Sep 11 19:26:59 2014 +0200
    36.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Thu Sep 11 19:32:36 2014 +0200
    36.3 @@ -15,7 +15,7 @@
    36.4  (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    36.5  (*********************************************************************************)
    36.6  
    36.7 -datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
    36.8 +datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
    36.9    | Mul int num
   36.10  
   36.11  primrec num_size :: "num \<Rightarrow> nat" -- {* A size for num to make inductive proofs simpler *}
   36.12 @@ -38,7 +38,7 @@
   36.13  | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
   36.14  | "Inum bs (Mul c a) = c* Inum bs a"
   36.15  
   36.16 -datatype_new fm  =
   36.17 +datatype fm  =
   36.18    T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
   36.19    NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
   36.20    | Closed nat | NClosed nat
    37.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Sep 11 19:26:59 2014 +0200
    37.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Thu Sep 11 19:32:36 2014 +0200
    37.3 @@ -13,7 +13,7 @@
    37.4    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    37.5    (*********************************************************************************)
    37.6  
    37.7 -datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 
    37.8 +datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 
    37.9    | Mul int num 
   37.10  
   37.11    (* A size for num to make inductive proofs simpler*)
   37.12 @@ -36,7 +36,7 @@
   37.13  | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
   37.14  | "Inum bs (Mul c a) = (real c) * Inum bs a"
   37.15      (* FORMULAE *)
   37.16 -datatype_new fm  = 
   37.17 +datatype fm  = 
   37.18    T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num|
   37.19    NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
   37.20  
    38.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Sep 11 19:26:59 2014 +0200
    38.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Thu Sep 11 19:32:36 2014 +0200
    38.3 @@ -105,7 +105,7 @@
    38.4    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    38.5    (*********************************************************************************)
    38.6  
    38.7 -datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 
    38.8 +datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 
    38.9    | Mul int num | Floor num| CF int num num
   38.10  
   38.11    (* A size for num to make inductive proofs simpler*)
   38.12 @@ -188,7 +188,7 @@
   38.13  
   38.14  
   38.15      (* FORMULAE *)
   38.16 -datatype_new fm  = 
   38.17 +datatype fm  = 
   38.18    T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
   38.19    NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
   38.20  
    39.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Sep 11 19:26:59 2014 +0200
    39.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Sep 11 19:32:36 2014 +0200
    39.3 @@ -15,7 +15,7 @@
    39.4  
    39.5  subsection {* Terms *}
    39.6  
    39.7 -datatype_new tm = CP poly | Bound nat | Add tm tm | Mul poly tm
    39.8 +datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm
    39.9    | Neg tm | Sub tm tm | CNP nat poly tm
   39.10  
   39.11  (* A size for poly to make inductive proofs simpler*)
   39.12 @@ -493,7 +493,7 @@
   39.13  
   39.14  subsection{* Formulae *}
   39.15  
   39.16 -datatype_new fm  =  T| F| Le tm | Lt tm | Eq tm | NEq tm|
   39.17 +datatype fm  =  T| F| Le tm | Lt tm | Eq tm | NEq tm|
   39.18    NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
   39.19  
   39.20  
    40.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Sep 11 19:26:59 2014 +0200
    40.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Sep 11 19:32:36 2014 +0200
    40.3 @@ -10,7 +10,7 @@
    40.4  
    40.5  subsection{* Datatype of polynomial expressions *}
    40.6  
    40.7 -datatype_new poly = C Num | Bound nat | Add poly poly | Sub poly poly
    40.8 +datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly
    40.9    | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
   40.10  
   40.11  abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
    41.1 --- a/src/HOL/Enum.thy	Thu Sep 11 19:26:59 2014 +0200
    41.2 +++ b/src/HOL/Enum.thy	Thu Sep 11 19:32:36 2014 +0200
    41.3 @@ -493,7 +493,7 @@
    41.4  
    41.5  text {* We define small finite types for the use in Quickcheck *}
    41.6  
    41.7 -datatype_new finite_1 = a\<^sub>1
    41.8 +datatype finite_1 = a\<^sub>1
    41.9  
   41.10  notation (output) a\<^sub>1  ("a\<^sub>1")
   41.11  
   41.12 @@ -595,7 +595,7 @@
   41.13  declare [[simproc del: finite_1_eq]]
   41.14  hide_const (open) a\<^sub>1
   41.15  
   41.16 -datatype_new finite_2 = a\<^sub>1 | a\<^sub>2
   41.17 +datatype finite_2 = a\<^sub>1 | a\<^sub>2
   41.18  
   41.19  notation (output) a\<^sub>1  ("a\<^sub>1")
   41.20  notation (output) a\<^sub>2  ("a\<^sub>2")
   41.21 @@ -701,7 +701,7 @@
   41.22  
   41.23  hide_const (open) a\<^sub>1 a\<^sub>2
   41.24  
   41.25 -datatype_new finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
   41.26 +datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
   41.27  
   41.28  notation (output) a\<^sub>1  ("a\<^sub>1")
   41.29  notation (output) a\<^sub>2  ("a\<^sub>2")
   41.30 @@ -825,7 +825,7 @@
   41.31  
   41.32  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
   41.33  
   41.34 -datatype_new finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
   41.35 +datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
   41.36  
   41.37  notation (output) a\<^sub>1  ("a\<^sub>1")
   41.38  notation (output) a\<^sub>2  ("a\<^sub>2")
   41.39 @@ -927,7 +927,7 @@
   41.40  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
   41.41  
   41.42  
   41.43 -datatype_new finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
   41.44 +datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
   41.45  
   41.46  notation (output) a\<^sub>1  ("a\<^sub>1")
   41.47  notation (output) a\<^sub>2  ("a\<^sub>2")
    42.1 --- a/src/HOL/Extraction.thy	Thu Sep 11 19:26:59 2014 +0200
    42.2 +++ b/src/HOL/Extraction.thy	Thu Sep 11 19:32:36 2014 +0200
    42.3 @@ -37,7 +37,7 @@
    42.4    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    42.5    induct_true_def induct_false_def
    42.6  
    42.7 -datatype_new sumbool = Left | Right
    42.8 +datatype sumbool = Left | Right
    42.9  
   42.10  subsection {* Type of extracted program *}
   42.11  
    43.1 --- a/src/HOL/HOLCF/Discrete.thy	Thu Sep 11 19:26:59 2014 +0200
    43.2 +++ b/src/HOL/HOLCF/Discrete.thy	Thu Sep 11 19:32:36 2014 +0200
    43.3 @@ -8,7 +8,7 @@
    43.4  imports Cont
    43.5  begin
    43.6  
    43.7 -datatype_new 'a discr = Discr "'a :: type"
    43.8 +datatype 'a discr = Discr "'a :: type"
    43.9  
   43.10  subsection {* Discrete cpo class instance *}
   43.11  
    44.1 --- a/src/HOL/HOLCF/FOCUS/Buffer.thy	Thu Sep 11 19:26:59 2014 +0200
    44.2 +++ b/src/HOL/HOLCF/FOCUS/Buffer.thy	Thu Sep 11 19:32:36 2014 +0200
    44.3 @@ -25,10 +25,10 @@
    44.4  
    44.5  typedecl D
    44.6  
    44.7 -datatype_new
    44.8 +datatype
    44.9    M     = Md D | Mreq ("\<bullet>")
   44.10  
   44.11 -datatype_new
   44.12 +datatype
   44.13    State = Sd D | Snil ("\<currency>")
   44.14  
   44.15  type_synonym
    45.1 --- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Thu Sep 11 19:26:59 2014 +0200
    45.2 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Thu Sep 11 19:32:36 2014 +0200
    45.3 @@ -8,7 +8,7 @@
    45.4  imports IOA Action Lemmas
    45.5  begin
    45.6  
    45.7 -datatype_new 'a abs_action = S 'a | R 'a
    45.8 +datatype 'a abs_action = S 'a | R 'a
    45.9  
   45.10  
   45.11  (**********************************************************
    46.1 --- a/src/HOL/HOLCF/IOA/ABP/Action.thy	Thu Sep 11 19:26:59 2014 +0200
    46.2 +++ b/src/HOL/HOLCF/IOA/ABP/Action.thy	Thu Sep 11 19:32:36 2014 +0200
    46.3 @@ -8,7 +8,7 @@
    46.4  imports Packet
    46.5  begin
    46.6  
    46.7 -datatype_new 'm action =
    46.8 +datatype 'm action =
    46.9      Next | S_msg 'm | R_msg 'm
   46.10    | S_pkt "'m packet" | R_pkt "'m packet"
   46.11    | S_ack bool | R_ack bool
    47.1 --- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Thu Sep 11 19:26:59 2014 +0200
    47.2 +++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Thu Sep 11 19:32:36 2014 +0200
    47.3 @@ -8,7 +8,7 @@
    47.4  imports IOA Action
    47.5  begin
    47.6  
    47.7 -datatype_new 'a abs_action = S 'a | R 'a
    47.8 +datatype 'a abs_action = S 'a | R 'a
    47.9  
   47.10  definition
   47.11    ch_asig :: "'a abs_action signature" where
    48.1 --- a/src/HOL/HOLCF/IOA/NTP/Action.thy	Thu Sep 11 19:26:59 2014 +0200
    48.2 +++ b/src/HOL/HOLCF/IOA/NTP/Action.thy	Thu Sep 11 19:32:36 2014 +0200
    48.3 @@ -8,7 +8,7 @@
    48.4  imports Packet
    48.5  begin
    48.6  
    48.7 -datatype_new 'm action = S_msg 'm | R_msg 'm
    48.8 +datatype 'm action = S_msg 'm | R_msg 'm
    48.9                     | S_pkt "'m packet" | R_pkt "'m packet"
   48.10                     | S_ack bool | R_ack bool
   48.11                     | C_m_s | C_m_r | C_r_s | C_r_r 'm
    49.1 --- a/src/HOL/HOLCF/IOA/Storage/Action.thy	Thu Sep 11 19:26:59 2014 +0200
    49.2 +++ b/src/HOL/HOLCF/IOA/Storage/Action.thy	Thu Sep 11 19:32:36 2014 +0200
    49.3 @@ -8,7 +8,7 @@
    49.4  imports Main
    49.5  begin
    49.6  
    49.7 -datatype_new action = New | Loc nat | Free nat
    49.8 +datatype action = New | Loc nat | Free nat
    49.9  
   49.10  lemma [cong]: "!!x. x = y ==> case_action a b c x = case_action a b c y"
   49.11    by simp
    50.1 --- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Thu Sep 11 19:26:59 2014 +0200
    50.2 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Thu Sep 11 19:32:36 2014 +0200
    50.3 @@ -8,7 +8,7 @@
    50.4  imports Abstraction
    50.5  begin
    50.6  
    50.7 -datatype_new action = INC
    50.8 +datatype action = INC
    50.9  
   50.10  definition
   50.11    C_asig :: "action signature" where
    51.1 --- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Thu Sep 11 19:26:59 2014 +0200
    51.2 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Thu Sep 11 19:32:36 2014 +0200
    51.3 @@ -8,7 +8,7 @@
    51.4  imports IOA Abstraction
    51.5  begin
    51.6  
    51.7 -datatype_new action = INC
    51.8 +datatype action = INC
    51.9  
   51.10  definition
   51.11    C_asig :: "action signature" where
    52.1 --- a/src/HOL/HOLCF/Up.thy	Thu Sep 11 19:26:59 2014 +0200
    52.2 +++ b/src/HOL/HOLCF/Up.thy	Thu Sep 11 19:32:36 2014 +0200
    52.3 @@ -13,7 +13,7 @@
    52.4  
    52.5  subsection {* Definition of new type for lifting *}
    52.6  
    52.7 -datatype_new 'a u = Ibottom | Iup 'a
    52.8 +datatype 'a u = Ibottom | Iup 'a
    52.9  
   52.10  type_notation (xsymbols)
   52.11    u  ("(_\<^sub>\<bottom>)" [1000] 999)
    53.1 --- a/src/HOL/Hoare/Heap.thy	Thu Sep 11 19:26:59 2014 +0200
    53.2 +++ b/src/HOL/Hoare/Heap.thy	Thu Sep 11 19:32:36 2014 +0200
    53.3 @@ -10,7 +10,7 @@
    53.4  
    53.5  subsection "References"
    53.6  
    53.7 -datatype_new 'a ref = Null | Ref 'a
    53.8 +datatype 'a ref = Null | Ref 'a
    53.9  
   53.10  lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
   53.11    by (induct x) auto
    54.1 --- a/src/HOL/Hoare/Hoare_Logic.thy	Thu Sep 11 19:26:59 2014 +0200
    54.2 +++ b/src/HOL/Hoare/Hoare_Logic.thy	Thu Sep 11 19:32:36 2014 +0200
    54.3 @@ -15,7 +15,7 @@
    54.4  type_synonym 'a bexp = "'a set"
    54.5  type_synonym 'a assn = "'a set"
    54.6  
    54.7 -datatype_new 'a com =
    54.8 +datatype 'a com =
    54.9    Basic "'a \<Rightarrow> 'a"
   54.10  | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
   54.11  | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
    55.1 --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Thu Sep 11 19:26:59 2014 +0200
    55.2 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Thu Sep 11 19:32:36 2014 +0200
    55.3 @@ -12,7 +12,7 @@
    55.4  type_synonym 'a bexp = "'a set"
    55.5  type_synonym 'a assn = "'a set"
    55.6  
    55.7 -datatype_new 'a com =
    55.8 +datatype 'a com =
    55.9    Basic "'a \<Rightarrow> 'a"
   55.10  | Abort
   55.11  | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
    56.1 --- a/src/HOL/Hoare_Parallel/Graph.thy	Thu Sep 11 19:26:59 2014 +0200
    56.2 +++ b/src/HOL/Hoare_Parallel/Graph.thy	Thu Sep 11 19:32:36 2014 +0200
    56.3 @@ -4,7 +4,7 @@
    56.4  
    56.5  theory Graph imports Main begin
    56.6  
    56.7 -datatype_new node = Black | White
    56.8 +datatype node = Black | White
    56.9  
   56.10  type_synonym nodes = "node list"
   56.11  type_synonym edge = "nat \<times> nat"
    57.1 --- a/src/HOL/Hoare_Parallel/OG_Com.thy	Thu Sep 11 19:26:59 2014 +0200
    57.2 +++ b/src/HOL/Hoare_Parallel/OG_Com.thy	Thu Sep 11 19:32:36 2014 +0200
    57.3 @@ -14,7 +14,7 @@
    57.4  datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a
    57.5  com"} for non-annotated commands. *}
    57.6  
    57.7 -datatype_new 'a ann_com = 
    57.8 +datatype 'a ann_com = 
    57.9       AnnBasic "('a assn)"  "('a \<Rightarrow> 'a)"         
   57.10     | AnnSeq "('a ann_com)"  "('a ann_com)"   
   57.11     | AnnCond1 "('a assn)"  "('a bexp)"  "('a ann_com)"  "('a ann_com)" 
    58.1 --- a/src/HOL/Hoare_Parallel/RG_Com.thy	Thu Sep 11 19:26:59 2014 +0200
    58.2 +++ b/src/HOL/Hoare_Parallel/RG_Com.thy	Thu Sep 11 19:32:36 2014 +0200
    58.3 @@ -12,7 +12,7 @@
    58.4  
    58.5  type_synonym 'a bexp = "'a set"
    58.6  
    58.7 -datatype_new 'a com = 
    58.8 +datatype 'a com = 
    58.9      Basic "'a \<Rightarrow>'a"
   58.10    | Seq "'a com" "'a com"
   58.11    | Cond "'a bexp" "'a com" "'a com"         
    59.1 --- a/src/HOL/IMP/ACom.thy	Thu Sep 11 19:26:59 2014 +0200
    59.2 +++ b/src/HOL/IMP/ACom.thy	Thu Sep 11 19:32:36 2014 +0200
    59.3 @@ -6,7 +6,7 @@
    59.4  
    59.5  subsection "Annotated Commands"
    59.6  
    59.7 -datatype_new 'a acom =
    59.8 +datatype 'a acom =
    59.9    SKIP 'a                           ("SKIP {_}" 61) |
   59.10    Assign vname aexp 'a              ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
   59.11    Seq "('a acom)" "('a acom)"       ("_;;//_"  [60, 61] 60) |
    60.1 --- a/src/HOL/IMP/AExp.thy	Thu Sep 11 19:26:59 2014 +0200
    60.2 +++ b/src/HOL/IMP/AExp.thy	Thu Sep 11 19:32:36 2014 +0200
    60.3 @@ -9,7 +9,7 @@
    60.4  type_synonym state = "vname \<Rightarrow> val"
    60.5  
    60.6  text_raw{*\snip{AExpaexpdef}{2}{1}{% *}
    60.7 -datatype_new aexp = N int | V vname | Plus aexp aexp
    60.8 +datatype aexp = N int | V vname | Plus aexp aexp
    60.9  text_raw{*}%endsnip*}
   60.10  
   60.11  text_raw{*\snip{AExpavaldef}{1}{2}{% *}
    61.1 --- a/src/HOL/IMP/ASM.thy	Thu Sep 11 19:26:59 2014 +0200
    61.2 +++ b/src/HOL/IMP/ASM.thy	Thu Sep 11 19:32:36 2014 +0200
    61.3 @@ -5,7 +5,7 @@
    61.4  subsection "Stack Machine"
    61.5  
    61.6  text_raw{*\snip{ASMinstrdef}{0}{1}{% *}
    61.7 -datatype_new instr = LOADI val | LOAD vname | ADD
    61.8 +datatype instr = LOADI val | LOAD vname | ADD
    61.9  text_raw{*}%endsnip*}
   61.10  
   61.11  text_raw{*\snip{ASMstackdef}{1}{2}{% *}
    62.1 --- a/src/HOL/IMP/Abs_Int1_const.thy	Thu Sep 11 19:26:59 2014 +0200
    62.2 +++ b/src/HOL/IMP/Abs_Int1_const.thy	Thu Sep 11 19:32:36 2014 +0200
    62.3 @@ -6,7 +6,7 @@
    62.4  
    62.5  subsection "Constant Propagation"
    62.6  
    62.7 -datatype_new const = Const val | Any
    62.8 +datatype const = Const val | Any
    62.9  
   62.10  fun \<gamma>_const where
   62.11  "\<gamma>_const (Const i) = {i}" |
    63.1 --- a/src/HOL/IMP/Abs_Int1_parity.thy	Thu Sep 11 19:26:59 2014 +0200
    63.2 +++ b/src/HOL/IMP/Abs_Int1_parity.thy	Thu Sep 11 19:32:36 2014 +0200
    63.3 @@ -6,7 +6,7 @@
    63.4  
    63.5  subsection "Parity Analysis"
    63.6  
    63.7 -datatype_new parity = Even | Odd | Either
    63.8 +datatype parity = Even | Odd | Either
    63.9  
   63.10  text{* Instantiation of class @{class order} with type @{typ parity}: *}
   63.11  
    64.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Thu Sep 11 19:26:59 2014 +0200
    64.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Thu Sep 11 19:32:36 2014 +0200
    64.3 @@ -6,7 +6,7 @@
    64.4  
    64.5  subsection "Constant Propagation"
    64.6  
    64.7 -datatype_new cval = Const val | Any
    64.8 +datatype cval = Const val | Any
    64.9  
   64.10  fun rep_cval where
   64.11  "rep_cval (Const n) = {n}" |
    65.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Thu Sep 11 19:26:59 2014 +0200
    65.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Thu Sep 11 19:32:36 2014 +0200
    65.3 @@ -6,7 +6,7 @@
    65.4  
    65.5  subsection "Interval Analysis"
    65.6  
    65.7 -datatype_new ivl = I "int option" "int option"
    65.8 +datatype ivl = I "int option" "int option"
    65.9  
   65.10  text{* We assume an important invariant: arithmetic operations are never
   65.11  applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j <
    66.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy	Thu Sep 11 19:26:59 2014 +0200
    66.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy	Thu Sep 11 19:32:36 2014 +0200
    66.3 @@ -10,7 +10,7 @@
    66.4  
    66.5  text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
    66.6  
    66.7 -datatype_new 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
    66.8 +datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
    66.9  
   66.10  fun "fun" where "fun (FunDom f _) = f"
   66.11  fun dom where "dom (FunDom _ A) = A"
    67.1 --- a/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy	Thu Sep 11 19:26:59 2014 +0200
    67.2 +++ b/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy	Thu Sep 11 19:32:36 2014 +0200
    67.3 @@ -6,7 +6,7 @@
    67.4  
    67.5  subsection "Annotated Commands"
    67.6  
    67.7 -datatype_new 'a acom =
    67.8 +datatype 'a acom =
    67.9    SKIP 'a                           ("SKIP {_}" 61) |
   67.10    Assign vname aexp 'a              ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
   67.11    Seq "('a acom)" "('a acom)"       ("_;;//_"  [60, 61] 60) |
    68.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Thu Sep 11 19:26:59 2014 +0200
    68.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Thu Sep 11 19:32:36 2014 +0200
    68.3 @@ -6,7 +6,7 @@
    68.4  
    68.5  subsection "Constant Propagation"
    68.6  
    68.7 -datatype_new const = Const val | Any
    68.8 +datatype const = Const val | Any
    68.9  
   68.10  fun \<gamma>_const where
   68.11  "\<gamma>_const (Const n) = {n}" |
    69.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Thu Sep 11 19:26:59 2014 +0200
    69.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Thu Sep 11 19:32:36 2014 +0200
    69.3 @@ -6,7 +6,7 @@
    69.4  
    69.5  subsection "Parity Analysis"
    69.6  
    69.7 -datatype_new parity = Even | Odd | Either
    69.8 +datatype parity = Even | Odd | Either
    69.9  
   69.10  text{* Instantiation of class @{class preord} with type @{typ parity}: *}
   69.11  
    70.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy	Thu Sep 11 19:26:59 2014 +0200
    70.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy	Thu Sep 11 19:32:36 2014 +0200
    70.3 @@ -6,7 +6,7 @@
    70.4  
    70.5  subsection "Interval Analysis"
    70.6  
    70.7 -datatype_new ivl = I "int option" "int option"
    70.8 +datatype ivl = I "int option" "int option"
    70.9  
   70.10  definition "\<gamma>_ivl i = (case i of
   70.11    I (Some l) (Some h) \<Rightarrow> {l..h} |
    71.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy	Thu Sep 11 19:26:59 2014 +0200
    71.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy	Thu Sep 11 19:32:36 2014 +0200
    71.3 @@ -10,7 +10,7 @@
    71.4  
    71.5  text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
    71.6  
    71.7 -datatype_new 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
    71.8 +datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
    71.9  
   71.10  fun "fun" where "fun (FunDom f xs) = f"
   71.11  fun dom where "dom (FunDom f xs) = xs"
    72.1 --- a/src/HOL/IMP/BExp.thy	Thu Sep 11 19:26:59 2014 +0200
    72.2 +++ b/src/HOL/IMP/BExp.thy	Thu Sep 11 19:32:36 2014 +0200
    72.3 @@ -2,7 +2,7 @@
    72.4  
    72.5  subsection "Boolean Expressions"
    72.6  
    72.7 -datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
    72.8 +datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
    72.9  
   72.10  text_raw{*\snip{BExpbvaldef}{1}{2}{% *}
   72.11  fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
    73.1 --- a/src/HOL/IMP/C_like.thy	Thu Sep 11 19:26:59 2014 +0200
    73.2 +++ b/src/HOL/IMP/C_like.thy	Thu Sep 11 19:32:36 2014 +0200
    73.3 @@ -4,14 +4,14 @@
    73.4  
    73.5  type_synonym state = "nat \<Rightarrow> nat"
    73.6  
    73.7 -datatype_new aexp = N nat | Deref aexp ("!") | Plus aexp aexp
    73.8 +datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp
    73.9  
   73.10  fun aval :: "aexp \<Rightarrow> state \<Rightarrow> nat" where
   73.11  "aval (N n) s = n" |
   73.12  "aval (!a) s = s(aval a s)" |
   73.13  "aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"
   73.14  
   73.15 -datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
   73.16 +datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
   73.17  
   73.18  primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
   73.19  "bval (Bc v) _ = v" |
   73.20 @@ -20,7 +20,7 @@
   73.21  "bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"
   73.22  
   73.23  
   73.24 -datatype_new
   73.25 +datatype
   73.26    com = SKIP 
   73.27        | Assign aexp aexp         ("_ ::= _" [61, 61] 61)
   73.28        | New    aexp aexp
    74.1 --- a/src/HOL/IMP/Com.thy	Thu Sep 11 19:26:59 2014 +0200
    74.2 +++ b/src/HOL/IMP/Com.thy	Thu Sep 11 19:32:36 2014 +0200
    74.3 @@ -2,7 +2,7 @@
    74.4  
    74.5  theory Com imports BExp begin
    74.6  
    74.7 -datatype_new
    74.8 +datatype
    74.9    com = SKIP 
   74.10        | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
   74.11        | Seq    com  com         ("_;;/ _"  [60, 61] 60)
    75.1 --- a/src/HOL/IMP/Compiler.thy	Thu Sep 11 19:26:59 2014 +0200
    75.2 +++ b/src/HOL/IMP/Compiler.thy	Thu Sep 11 19:32:36 2014 +0200
    75.3 @@ -43,7 +43,7 @@
    75.4  subsection "Instructions and Stack Machine"
    75.5  
    75.6  text_raw{*\snip{instrdef}{0}{1}{% *}
    75.7 -datatype_new instr = 
    75.8 +datatype instr = 
    75.9    LOADI int | LOAD vname | ADD | STORE vname |
   75.10    JMP int | JMPLESS int | JMPGE int
   75.11  text_raw{*}%endsnip*}
    76.1 --- a/src/HOL/IMP/OO.thy	Thu Sep 11 19:26:59 2014 +0200
    76.2 +++ b/src/HOL/IMP/OO.thy	Thu Sep 11 19:32:36 2014 +0200
    76.3 @@ -8,13 +8,13 @@
    76.4  where "f(x,y := z) == f(x := (f x)(y := z))"
    76.5  
    76.6  type_synonym addr = nat
    76.7 -datatype_new ref = null | Ref addr
    76.8 +datatype ref = null | Ref addr
    76.9  
   76.10  type_synonym obj = "string \<Rightarrow> ref"
   76.11  type_synonym venv = "string \<Rightarrow> ref"
   76.12  type_synonym store = "addr \<Rightarrow> obj"
   76.13  
   76.14 -datatype_new exp =
   76.15 +datatype exp =
   76.16    Null |
   76.17    New |
   76.18    V string |
    77.1 --- a/src/HOL/IMP/Poly_Types.thy	Thu Sep 11 19:26:59 2014 +0200
    77.2 +++ b/src/HOL/IMP/Poly_Types.thy	Thu Sep 11 19:32:36 2014 +0200
    77.3 @@ -2,7 +2,7 @@
    77.4  
    77.5  subsection "Type Variables"
    77.6  
    77.7 -datatype_new ty = Ity | Rty | TV nat
    77.8 +datatype ty = Ity | Rty | TV nat
    77.9  
   77.10  text{* Everything else remains the same. *}
   77.11  
    78.1 --- a/src/HOL/IMP/Procs.thy	Thu Sep 11 19:26:59 2014 +0200
    78.2 +++ b/src/HOL/IMP/Procs.thy	Thu Sep 11 19:32:36 2014 +0200
    78.3 @@ -6,7 +6,7 @@
    78.4  
    78.5  type_synonym pname = string
    78.6  
    78.7 -datatype_new
    78.8 +datatype
    78.9    com = SKIP 
   78.10        | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
   78.11        | Seq    com  com          ("_;;/ _"  [60, 61] 60)
    79.1 --- a/src/HOL/IMP/Types.thy	Thu Sep 11 19:26:59 2014 +0200
    79.2 +++ b/src/HOL/IMP/Types.thy	Thu Sep 11 19:32:36 2014 +0200
    79.3 @@ -7,13 +7,13 @@
    79.4  
    79.5  subsection "Arithmetic Expressions"
    79.6  
    79.7 -datatype_new val = Iv int | Rv real
    79.8 +datatype val = Iv int | Rv real
    79.9  
   79.10  type_synonym vname = string
   79.11  type_synonym state = "vname \<Rightarrow> val"
   79.12  
   79.13  text_raw{*\snip{aexptDef}{0}{2}{% *}
   79.14 -datatype_new aexp =  Ic int | Rc real | V vname | Plus aexp aexp
   79.15 +datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp
   79.16  text_raw{*}%endsnip*}
   79.17  
   79.18  inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
   79.19 @@ -32,7 +32,7 @@
   79.20  
   79.21  subsection "Boolean Expressions"
   79.22  
   79.23 -datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
   79.24 +datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
   79.25  
   79.26  inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
   79.27  "tbval (Bc v) s v" |
   79.28 @@ -44,7 +44,7 @@
   79.29  subsection "Syntax of Commands"
   79.30  (* a copy of Com.thy - keep in sync! *)
   79.31  
   79.32 -datatype_new
   79.33 +datatype
   79.34    com = SKIP 
   79.35        | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
   79.36        | Seq    com  com         ("_;; _"  [60, 61] 60)
   79.37 @@ -71,7 +71,7 @@
   79.38  
   79.39  subsection "The Type System"
   79.40  
   79.41 -datatype_new ty = Ity | Rty
   79.42 +datatype ty = Ity | Rty
   79.43  
   79.44  type_synonym tyenv = "vname \<Rightarrow> ty"
   79.45  
    80.1 --- a/src/HOL/IMP/VCG.thy	Thu Sep 11 19:26:59 2014 +0200
    80.2 +++ b/src/HOL/IMP/VCG.thy	Thu Sep 11 19:32:36 2014 +0200
    80.3 @@ -7,7 +7,7 @@
    80.4  text{* Annotated commands: commands where loops are annotated with
    80.5  invariants. *}
    80.6  
    80.7 -datatype_new acom =
    80.8 +datatype acom =
    80.9    Askip                  ("SKIP") |
   80.10    Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
   80.11    Aseq   acom acom       ("_;;/ _"  [60, 61] 60) |
    81.1 --- a/src/HOL/IMPP/Com.thy	Thu Sep 11 19:26:59 2014 +0200
    81.2 +++ b/src/HOL/IMPP/Com.thy	Thu Sep 11 19:32:36 2014 +0200
    81.3 @@ -18,10 +18,10 @@
    81.4    Arg :: loc and
    81.5    Res :: loc
    81.6  
    81.7 -datatype_new vname  = Glb glb | Loc loc
    81.8 +datatype vname  = Glb glb | Loc loc
    81.9  type_synonym globs = "glb => val"
   81.10  type_synonym locals = "loc => val"
   81.11 -datatype_new state  = st globs locals
   81.12 +datatype state  = st globs locals
   81.13  (* for the meta theory, the following would be sufficient:
   81.14  typedecl state
   81.15  consts   st :: "[globs , locals] => state"
   81.16 @@ -31,7 +31,7 @@
   81.17  
   81.18  typedecl pname
   81.19  
   81.20 -datatype_new com
   81.21 +datatype com
   81.22        = SKIP
   81.23        | Ass   vname aexp        ("_:==_"                [65, 65    ] 60)
   81.24        | Local loc aexp com      ("LOCAL _:=_ IN _"      [65,  0, 61] 60)
    82.1 --- a/src/HOL/IMPP/Hoare.thy	Thu Sep 11 19:26:59 2014 +0200
    82.2 +++ b/src/HOL/IMPP/Hoare.thy	Thu Sep 11 19:32:36 2014 +0200
    82.3 @@ -28,7 +28,7 @@
    82.4    peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35) where
    82.5    "peek_and P p = (%Z s. P Z s & p s)"
    82.6  
    82.7 -datatype_new 'a triple =
    82.8 +datatype 'a triple =
    82.9    triple "'a assn"  com  "'a assn"       ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58)
   82.10  
   82.11  definition
    83.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Sep 11 19:26:59 2014 +0200
    83.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Sep 11 19:32:36 2014 +0200
    83.3 @@ -16,7 +16,7 @@
    83.4  
    83.5  text {* Monadic heap actions either produce values
    83.6    and transform the heap, or fail *}
    83.7 -datatype_new 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
    83.8 +datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
    83.9  
   83.10  lemma [code, code del]:
   83.11    "(Code_Evaluation.term_of :: 'a::typerep Heap \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of"
    84.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Thu Sep 11 19:26:59 2014 +0200
    84.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Thu Sep 11 19:32:36 2014 +0200
    84.3 @@ -20,7 +20,7 @@
    84.4  text {* This resembles exactly to Isat's Proof Steps *}
    84.5  
    84.6  type_synonym Resolvants = "ClauseId * (Lit * ClauseId) list"
    84.7 -datatype_new ProofStep =
    84.8 +datatype ProofStep =
    84.9    ProofDone bool
   84.10    | Root ClauseId Clause
   84.11    | Conflict ClauseId Resolvants
    85.1 --- a/src/HOL/Induct/ABexp.thy	Thu Sep 11 19:26:59 2014 +0200
    85.2 +++ b/src/HOL/Induct/ABexp.thy	Thu Sep 11 19:32:36 2014 +0200
    85.3 @@ -8,7 +8,7 @@
    85.4  imports Main
    85.5  begin
    85.6  
    85.7 -datatype_new 'a aexp =
    85.8 +datatype 'a aexp =
    85.9      IF "'a bexp"  "'a aexp"  "'a aexp"
   85.10    | Sum "'a aexp"  "'a aexp"
   85.11    | Diff "'a aexp"  "'a aexp"
    86.1 --- a/src/HOL/Induct/Com.thy	Thu Sep 11 19:26:59 2014 +0200
    86.2 +++ b/src/HOL/Induct/Com.thy	Thu Sep 11 19:32:36 2014 +0200
    86.3 @@ -12,7 +12,7 @@
    86.4  typedecl loc
    86.5  type_synonym state = "loc => nat"
    86.6  
    86.7 -datatype_new
    86.8 +datatype
    86.9    exp = N nat
   86.10        | X loc
   86.11        | Op "nat => nat => nat" exp exp
    87.1 --- a/src/HOL/Induct/Comb.thy	Thu Sep 11 19:26:59 2014 +0200
    87.2 +++ b/src/HOL/Induct/Comb.thy	Thu Sep 11 19:32:36 2014 +0200
    87.3 @@ -20,7 +20,7 @@
    87.4  
    87.5  text {* Datatype definition of combinators @{text S} and @{text K}. *}
    87.6  
    87.7 -datatype_new comb = K
    87.8 +datatype comb = K
    87.9                | S
   87.10                | Ap comb comb (infixl "##" 90)
   87.11  
    88.1 --- a/src/HOL/Induct/Common_Patterns.thy	Thu Sep 11 19:26:59 2014 +0200
    88.2 +++ b/src/HOL/Induct/Common_Patterns.thy	Thu Sep 11 19:32:36 2014 +0200
    88.3 @@ -218,7 +218,7 @@
    88.4    before!
    88.5  *}
    88.6  
    88.7 -datatype_new foo = Foo1 nat | Foo2 bar
    88.8 +datatype foo = Foo1 nat | Foo2 bar
    88.9    and bar = Bar1 bool | Bar2 bazar
   88.10    and bazar = Bazar foo
   88.11  
    89.1 --- a/src/HOL/Induct/Ordinals.thy	Thu Sep 11 19:26:59 2014 +0200
    89.2 +++ b/src/HOL/Induct/Ordinals.thy	Thu Sep 11 19:32:36 2014 +0200
    89.3 @@ -14,7 +14,7 @@
    89.4    @{url "http://www.dcs.ed.ac.uk/home/pgh/chat.html"}).
    89.5  *}
    89.6  
    89.7 -datatype_new ordinal =
    89.8 +datatype ordinal =
    89.9      Zero
   89.10    | Succ ordinal
   89.11    | Limit "nat => ordinal"
    90.1 --- a/src/HOL/Induct/PropLog.thy	Thu Sep 11 19:26:59 2014 +0200
    90.2 +++ b/src/HOL/Induct/PropLog.thy	Thu Sep 11 19:32:36 2014 +0200
    90.3 @@ -20,7 +20,7 @@
    90.4  
    90.5  subsection {* The datatype of propositions *}
    90.6  
    90.7 -datatype_new 'a pl =
    90.8 +datatype 'a pl =
    90.9    false |
   90.10    var 'a ("#_" [1000]) |
   90.11    imp "'a pl" "'a pl" (infixr "->" 90)
    91.1 --- a/src/HOL/Induct/QuoDataType.thy	Thu Sep 11 19:26:59 2014 +0200
    91.2 +++ b/src/HOL/Induct/QuoDataType.thy	Thu Sep 11 19:32:36 2014 +0200
    91.3 @@ -10,7 +10,7 @@
    91.4  subsection{*Defining the Free Algebra*}
    91.5  
    91.6  text{*Messages with encryption and decryption as free constructors.*}
    91.7 -datatype_new
    91.8 +datatype
    91.9       freemsg = NONCE  nat
   91.10               | MPAIR  freemsg freemsg
   91.11               | CRYPT  nat freemsg  
    92.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Thu Sep 11 19:26:59 2014 +0200
    92.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Thu Sep 11 19:32:36 2014 +0200
    92.3 @@ -10,7 +10,7 @@
    92.4  subsection{*Defining the Free Algebra*}
    92.5  
    92.6  text{*Messages with encryption and decryption as free constructors.*}
    92.7 -datatype_new
    92.8 +datatype
    92.9       freeExp = VAR  nat
   92.10               | PLUS  freeExp freeExp
   92.11               | FNCALL  nat "freeExp list"
    93.1 --- a/src/HOL/Induct/Term.thy	Thu Sep 11 19:26:59 2014 +0200
    93.2 +++ b/src/HOL/Induct/Term.thy	Thu Sep 11 19:32:36 2014 +0200
    93.3 @@ -8,7 +8,7 @@
    93.4  imports Main
    93.5  begin
    93.6  
    93.7 -datatype_new ('a, 'b) "term" =
    93.8 +datatype ('a, 'b) "term" =
    93.9      Var 'a
   93.10    | App 'b "('a, 'b) term list"
   93.11  
    94.1 --- a/src/HOL/Induct/Tree.thy	Thu Sep 11 19:26:59 2014 +0200
    94.2 +++ b/src/HOL/Induct/Tree.thy	Thu Sep 11 19:32:36 2014 +0200
    94.3 @@ -9,7 +9,7 @@
    94.4  imports Main
    94.5  begin
    94.6  
    94.7 -datatype_new 'a tree =
    94.8 +datatype 'a tree =
    94.9      Atom 'a
   94.10    | Branch "nat => 'a tree"
   94.11  
   94.12 @@ -34,7 +34,7 @@
   94.13  
   94.14  subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
   94.15  
   94.16 -datatype_new brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
   94.17 +datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
   94.18  
   94.19  text{*Addition of ordinals*}
   94.20  primrec add :: "[brouwer,brouwer] => brouwer"
    95.1 --- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Thu Sep 11 19:26:59 2014 +0200
    95.2 +++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Thu Sep 11 19:32:36 2014 +0200
    95.3 @@ -31,7 +31,7 @@
    95.4    consisting of variables, constants, and binary operations on
    95.5    expressions. *}
    95.6  
    95.7 -datatype_new (dead 'adr, dead 'val) expr =
    95.8 +datatype (dead 'adr, dead 'val) expr =
    95.9      Variable 'adr
   95.10    | Constant 'val
   95.11    | Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
   95.12 @@ -51,7 +51,7 @@
   95.13  text {* Next we model a simple stack machine, with three
   95.14    instructions. *}
   95.15  
   95.16 -datatype_new (dead 'adr, dead 'val) instr =
   95.17 +datatype (dead 'adr, dead 'val) instr =
   95.18      Const 'val
   95.19    | Load 'adr
   95.20    | Apply "'val binop"
    96.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Thu Sep 11 19:26:59 2014 +0200
    96.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Thu Sep 11 19:32:36 2014 +0200
    96.3 @@ -21,7 +21,7 @@
    96.4  type_synonym 'a bexp = "'a set"
    96.5  type_synonym 'a assn = "'a set"
    96.6  
    96.7 -datatype_new 'a com =
    96.8 +datatype 'a com =
    96.9      Basic "'a \<Rightarrow> 'a"
   96.10    | Seq "'a com" "'a com"    ("(_;/ _)" [60, 61] 60)
   96.11    | Cond "'a bexp" "'a com" "'a com"
    97.1 --- a/src/HOL/Isar_Examples/Nested_Datatype.thy	Thu Sep 11 19:26:59 2014 +0200
    97.2 +++ b/src/HOL/Isar_Examples/Nested_Datatype.thy	Thu Sep 11 19:32:36 2014 +0200
    97.3 @@ -6,7 +6,7 @@
    97.4  
    97.5  subsection {* Terms and substitution *}
    97.6  
    97.7 -datatype_new ('a, 'b) "term" =
    97.8 +datatype ('a, 'b) "term" =
    97.9    Var 'a
   97.10  | App 'b "('a, 'b) term list"
   97.11  
    98.1 --- a/src/HOL/Lattice/Orders.thy	Thu Sep 11 19:26:59 2014 +0200
    98.2 +++ b/src/HOL/Lattice/Orders.thy	Thu Sep 11 19:32:36 2014 +0200
    98.3 @@ -46,7 +46,7 @@
    98.4    of the original one.
    98.5  *}
    98.6  
    98.7 -datatype_new 'a dual = dual 'a
    98.8 +datatype 'a dual = dual 'a
    98.9  
   98.10  primrec undual :: "'a dual \<Rightarrow> 'a" where
   98.11    undual_dual: "undual (dual x) = x"
    99.1 --- a/src/HOL/Lazy_Sequence.thy	Thu Sep 11 19:26:59 2014 +0200
    99.2 +++ b/src/HOL/Lazy_Sequence.thy	Thu Sep 11 19:32:36 2014 +0200
    99.3 @@ -9,7 +9,7 @@
    99.4  
    99.5  subsection {* Type of lazy sequences *}
    99.6  
    99.7 -datatype_new (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
    99.8 +datatype (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
    99.9  
   99.10  primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
   99.11  where
   100.1 --- a/src/HOL/Library/Extended.thy	Thu Sep 11 19:26:59 2014 +0200
   100.2 +++ b/src/HOL/Library/Extended.thy	Thu Sep 11 19:32:36 2014 +0200
   100.3 @@ -10,7 +10,7 @@
   100.4    "~~/src/HOL/Library/Simps_Case_Conv"
   100.5  begin
   100.6  
   100.7 -datatype_new 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
   100.8 +datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
   100.9  
  100.10  
  100.11  instantiation extended :: (order)order
   101.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Sep 11 19:26:59 2014 +0200
   101.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Sep 11 19:32:36 2014 +0200
   101.3 @@ -20,7 +20,7 @@
   101.4  
   101.5  subsection {* Definition and basic properties *}
   101.6  
   101.7 -datatype_new ereal = ereal real | PInfty | MInfty
   101.8 +datatype ereal = ereal real | PInfty | MInfty
   101.9  
  101.10  instantiation ereal :: uminus
  101.11  begin
   102.1 --- a/src/HOL/Library/IArray.thy	Thu Sep 11 19:26:59 2014 +0200
   102.2 +++ b/src/HOL/Library/IArray.thy	Thu Sep 11 19:32:36 2014 +0200
   102.3 @@ -13,7 +13,7 @@
   102.4  lists first. Arrays could be converted back into lists for printing if they
   102.5  were wrapped up in an additional constructor. *}
   102.6  
   102.7 -datatype_new 'a iarray = IArray "'a list"
   102.8 +datatype 'a iarray = IArray "'a list"
   102.9  
  102.10  primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
  102.11  "list_of (IArray xs) = xs"
   103.1 --- a/src/HOL/Library/Lattice_Constructions.thy	Thu Sep 11 19:26:59 2014 +0200
   103.2 +++ b/src/HOL/Library/Lattice_Constructions.thy	Thu Sep 11 19:32:36 2014 +0200
   103.3 @@ -9,7 +9,7 @@
   103.4  
   103.5  subsection {* Values extended by a bottom element *}
   103.6  
   103.7 -datatype_new 'a bot = Value 'a | Bot
   103.8 +datatype 'a bot = Value 'a | Bot
   103.9  
  103.10  instantiation bot :: (preorder) preorder
  103.11  begin
  103.12 @@ -108,7 +108,7 @@
  103.13  
  103.14  section {* Values extended by a top element *}
  103.15  
  103.16 -datatype_new 'a top = Value 'a | Top
  103.17 +datatype 'a top = Value 'a | Top
  103.18  
  103.19  instantiation top :: (preorder) preorder
  103.20  begin
  103.21 @@ -207,7 +207,7 @@
  103.22  
  103.23  subsection {* Values extended by a top and a bottom element *}
  103.24  
  103.25 -datatype_new 'a flat_complete_lattice = Value 'a | Bot | Top
  103.26 +datatype 'a flat_complete_lattice = Value 'a | Bot | Top
  103.27  
  103.28  instantiation flat_complete_lattice :: (type) order
  103.29  begin
   104.1 --- a/src/HOL/Library/Parallel.thy	Thu Sep 11 19:26:59 2014 +0200
   104.2 +++ b/src/HOL/Library/Parallel.thy	Thu Sep 11 19:32:36 2014 +0200
   104.3 @@ -8,7 +8,7 @@
   104.4  
   104.5  subsection {* Futures *}
   104.6  
   104.7 -datatype_new 'a future = fork "unit \<Rightarrow> 'a"
   104.8 +datatype 'a future = fork "unit \<Rightarrow> 'a"
   104.9  
  104.10  primrec join :: "'a future \<Rightarrow> 'a" where
  104.11    "join (fork f) = f ()"
   105.1 --- a/src/HOL/Library/Phantom_Type.thy	Thu Sep 11 19:26:59 2014 +0200
   105.2 +++ b/src/HOL/Library/Phantom_Type.thy	Thu Sep 11 19:32:36 2014 +0200
   105.3 @@ -8,7 +8,7 @@
   105.4  imports Main
   105.5  begin
   105.6  
   105.7 -datatype_new ('a, 'b) phantom = phantom 'b
   105.8 +datatype ('a, 'b) phantom = phantom 'b
   105.9  
  105.10  primrec of_phantom :: "('a, 'b) phantom \<Rightarrow> 'b" 
  105.11  where "of_phantom (phantom x) = x"
   106.1 --- a/src/HOL/Library/RBT_Impl.thy	Thu Sep 11 19:26:59 2014 +0200
   106.2 +++ b/src/HOL/Library/RBT_Impl.thy	Thu Sep 11 19:32:36 2014 +0200
   106.3 @@ -16,8 +16,8 @@
   106.4  
   106.5  subsection {* Datatype of RB trees *}
   106.6  
   106.7 -datatype_new color = R | B
   106.8 -datatype_new ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
   106.9 +datatype color = R | B
  106.10 +datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
  106.11  
  106.12  lemma rbt_cases:
  106.13    obtains (Empty) "t = Empty" 
  106.14 @@ -1728,7 +1728,7 @@
  106.15  where
  106.16    "skip_black t = (let t' = skip_red t in case t' of Branch color.B l k v r \<Rightarrow> l | _ \<Rightarrow> t')"
  106.17  
  106.18 -datatype_new compare = LT | GT | EQ
  106.19 +datatype compare = LT | GT | EQ
  106.20  
  106.21  partial_function (tailrec) compare_height :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> compare"
  106.22  where
   107.1 --- a/src/HOL/Library/Tree.thy	Thu Sep 11 19:26:59 2014 +0200
   107.2 +++ b/src/HOL/Library/Tree.thy	Thu Sep 11 19:32:36 2014 +0200
   107.3 @@ -6,7 +6,7 @@
   107.4  imports Main
   107.5  begin
   107.6  
   107.7 -datatype_new 'a tree = Leaf | Node (left: "'a tree") (val: 'a) (right: "'a tree")
   107.8 +datatype 'a tree = Leaf | Node (left: "'a tree") (val: 'a) (right: "'a tree")
   107.9    where
  107.10      "left Leaf = Leaf"
  107.11    | "right Leaf = Leaf"
   108.1 --- a/src/HOL/List.thy	Thu Sep 11 19:26:59 2014 +0200
   108.2 +++ b/src/HOL/List.thy	Thu Sep 11 19:32:36 2014 +0200
   108.3 @@ -8,7 +8,7 @@
   108.4  imports Sledgehammer Code_Numeral Lifting_Set Lifting_Option Lifting_Product
   108.5  begin
   108.6  
   108.7 -datatype_new (set: 'a) list =
   108.8 +datatype (set: 'a) list =
   108.9      Nil  ("[]")
  108.10    | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
  108.11  for
   109.1 --- a/src/HOL/Metis_Examples/Binary_Tree.thy	Thu Sep 11 19:26:59 2014 +0200
   109.2 +++ b/src/HOL/Metis_Examples/Binary_Tree.thy	Thu Sep 11 19:32:36 2014 +0200
   109.3 @@ -13,7 +13,7 @@
   109.4  
   109.5  declare [[metis_new_skolem]]
   109.6  
   109.7 -datatype_new 'a bt =
   109.8 +datatype 'a bt =
   109.9      Lf
  109.10    | Br 'a  "'a bt"  "'a bt"
  109.11  
   110.1 --- a/src/HOL/Metis_Examples/Message.thy	Thu Sep 11 19:26:59 2014 +0200
   110.2 +++ b/src/HOL/Metis_Examples/Message.thy	Thu Sep 11 19:32:36 2014 +0200
   110.3 @@ -34,10 +34,10 @@
   110.4  definition symKeys :: "key set" where
   110.5    "symKeys == {K. invKey K = K}"
   110.6  
   110.7 -datatype_new  --{*We allow any number of friendly agents*}
   110.8 +datatype  --{*We allow any number of friendly agents*}
   110.9    agent = Server | Friend nat | Spy
  110.10  
  110.11 -datatype_new
  110.12 +datatype
  110.13       msg = Agent  agent     --{*Agent names*}
  110.14           | Number nat       --{*Ordinary integers, timestamps, ...*}
  110.15           | Nonce  nat       --{*Unguessable nonces*}
   111.1 --- a/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Sep 11 19:26:59 2014 +0200
   111.2 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Sep 11 19:32:36 2014 +0200
   111.3 @@ -15,7 +15,7 @@
   111.4  
   111.5  type_synonym addr = nat
   111.6  
   111.7 -datatype_new val
   111.8 +datatype val
   111.9    = Unit        -- "dummy result value of void expressions"
  111.10    | Null        -- "null reference"
  111.11    | Bool bool   -- "Boolean value"
   112.1 --- a/src/HOL/MicroJava/DFA/Err.thy	Thu Sep 11 19:26:59 2014 +0200
   112.2 +++ b/src/HOL/MicroJava/DFA/Err.thy	Thu Sep 11 19:32:36 2014 +0200
   112.3 @@ -9,7 +9,7 @@
   112.4  imports Semilat
   112.5  begin
   112.6  
   112.7 -datatype_new 'a err = Err | OK 'a
   112.8 +datatype 'a err = Err | OK 'a
   112.9  
  112.10  type_synonym 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
  112.11  type_synonym 'a esl = "'a set * 'a ord * 'a ebinop"
   113.1 --- a/src/HOL/MicroJava/J/Example.thy	Thu Sep 11 19:26:59 2014 +0200
   113.2 +++ b/src/HOL/MicroJava/J/Example.thy	Thu Sep 11 19:32:36 2014 +0200
   113.3 @@ -36,8 +36,8 @@
   113.4  \end{verbatim}
   113.5  *}
   113.6  
   113.7 -datatype_new cnam' = Base' | Ext'
   113.8 -datatype_new vnam' = vee' | x' | e'
   113.9 +datatype cnam' = Base' | Ext'
  113.10 +datatype vnam' = vee' | x' | e'
  113.11  
  113.12  text {*
  113.13    @{text cnam'} and @{text vnam'} are intended to be isomorphic 
   114.1 --- a/src/HOL/MicroJava/J/Term.thy	Thu Sep 11 19:26:59 2014 +0200
   114.2 +++ b/src/HOL/MicroJava/J/Term.thy	Thu Sep 11 19:32:36 2014 +0200
   114.3 @@ -6,9 +6,9 @@
   114.4  
   114.5  theory Term imports Value begin
   114.6  
   114.7 -datatype_new binop = Eq | Add    -- "function codes for binary operation"
   114.8 +datatype binop = Eq | Add    -- "function codes for binary operation"
   114.9  
  114.10 -datatype_new expr
  114.11 +datatype expr
  114.12    = NewC cname               -- "class instance creation"
  114.13    | Cast cname expr          -- "type cast"
  114.14    | Lit val                  -- "literal value, also references"
  114.15 @@ -23,7 +23,7 @@
  114.16  
  114.17  datatype_compat expr
  114.18  
  114.19 -datatype_new stmt
  114.20 +datatype stmt
  114.21    = Skip                     -- "empty statement"
  114.22    | Expr expr                -- "expression statement"
  114.23    | Comp stmt stmt       ("_;; _"             [61,60]60)
   115.1 --- a/src/HOL/MicroJava/J/Type.thy	Thu Sep 11 19:26:59 2014 +0200
   115.2 +++ b/src/HOL/MicroJava/J/Type.thy	Thu Sep 11 19:32:36 2014 +0200
   115.3 @@ -45,14 +45,14 @@
   115.4  end
   115.5  
   115.6   -- "exceptions"
   115.7 -datatype_new 
   115.8 +datatype 
   115.9    xcpt   
  115.10    = NullPointer
  115.11    | ClassCast
  115.12    | OutOfMemory
  115.13  
  115.14  -- "class names"
  115.15 -datatype_new cname  
  115.16 +datatype cname  
  115.17    = Object 
  115.18    | Xcpt xcpt 
  115.19    | Cname cnam 
  115.20 @@ -128,23 +128,23 @@
  115.21  end
  115.22  
  115.23  -- "names for @{text This} pointer and local/field variables"
  115.24 -datatype_new vname 
  115.25 +datatype vname 
  115.26    = This
  115.27    | VName vnam
  115.28  
  115.29  -- "primitive type, cf. 4.2"
  115.30 -datatype_new prim_ty 
  115.31 +datatype prim_ty 
  115.32    = Void          -- "'result type' of void methods"
  115.33    | Boolean
  115.34    | Integer
  115.35  
  115.36  -- "reference type, cf. 4.3"
  115.37 -datatype_new ref_ty   
  115.38 +datatype ref_ty   
  115.39    = NullT         -- "null type, cf. 4.1"
  115.40    | ClassT cname  -- "class type"
  115.41  
  115.42  -- "any type, cf. 4.1"
  115.43 -datatype_new ty 
  115.44 +datatype ty 
  115.45    = PrimT prim_ty -- "primitive type"
  115.46    | RefT  ref_ty  -- "reference type"
  115.47  
   116.1 --- a/src/HOL/MicroJava/J/Value.thy	Thu Sep 11 19:26:59 2014 +0200
   116.2 +++ b/src/HOL/MicroJava/J/Value.thy	Thu Sep 11 19:32:36 2014 +0200
   116.3 @@ -8,11 +8,11 @@
   116.4  
   116.5  typedecl loc' -- "locations, i.e. abstract references on objects" 
   116.6  
   116.7 -datatype_new loc 
   116.8 +datatype loc 
   116.9    = XcptRef xcpt -- "special locations for pre-allocated system exceptions"
  116.10    | Loc loc'     -- "usual locations (references on objects)"
  116.11  
  116.12 -datatype_new val
  116.13 +datatype val
  116.14    = Unit        -- "dummy result value of void methods"
  116.15    | Null        -- "null reference"
  116.16    | Bool bool   -- "Boolean value"
   117.1 --- a/src/HOL/MicroJava/JVM/JVMDefensive.thy	Thu Sep 11 19:26:59 2014 +0200
   117.2 +++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy	Thu Sep 11 19:32:36 2014 +0200
   117.3 @@ -11,7 +11,7 @@
   117.4  text {*
   117.5    Extend the state space by one element indicating a type error (or
   117.6    other abnormal termination) *}
   117.7 -datatype_new 'a type_error = TypeError | Normal 'a
   117.8 +datatype 'a type_error = TypeError | Normal 'a
   117.9  
  117.10  
  117.11  abbreviation
   118.1 --- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Thu Sep 11 19:26:59 2014 +0200
   118.2 +++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Thu Sep 11 19:32:36 2014 +0200
   118.3 @@ -8,7 +8,7 @@
   118.4  theory JVMInstructions imports JVMState begin
   118.5  
   118.6  
   118.7 -datatype_new 
   118.8 +datatype 
   118.9    instr = Load nat                  -- "load from local variable"
  118.10          | Store nat                 -- "store into local variable"
  118.11          | LitPush val               -- "push a literal (constant)"
   119.1 --- a/src/HOL/NanoJava/Decl.thy	Thu Sep 11 19:26:59 2014 +0200
   119.2 +++ b/src/HOL/NanoJava/Decl.thy	Thu Sep 11 19:32:36 2014 +0200
   119.3 @@ -7,7 +7,7 @@
   119.4  
   119.5  theory Decl imports Term begin
   119.6  
   119.7 -datatype_new ty
   119.8 +datatype ty
   119.9    = NT           --{* null type  *}
  119.10    | Class cname  --{* class type *}
  119.11  
   120.1 --- a/src/HOL/NanoJava/State.thy	Thu Sep 11 19:26:59 2014 +0200
   120.2 +++ b/src/HOL/NanoJava/State.thy	Thu Sep 11 19:32:36 2014 +0200
   120.3 @@ -13,7 +13,7 @@
   120.4  text {* Locations, i.e.\ abstract references to objects *}
   120.5  typedecl loc 
   120.6  
   120.7 -datatype_new val
   120.8 +datatype val
   120.9    = Null        --{* null reference *}
  120.10    | Addr loc    --{* address, i.e. location of object *}
  120.11  
   121.1 --- a/src/HOL/NanoJava/Term.thy	Thu Sep 11 19:26:59 2014 +0200
   121.2 +++ b/src/HOL/NanoJava/Term.thy	Thu Sep 11 19:32:36 2014 +0200
   121.3 @@ -23,7 +23,7 @@
   121.4    Res_neq_This [simp]: "Res \<noteq> This"
   121.5  *)
   121.6  
   121.7 -datatype_new stmt
   121.8 +datatype stmt
   121.9    = Skip                   --{* empty statement *}
  121.10    | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
  121.11    | Cond expr  stmt stmt   ("If '(_') _ Else _" [ 3,91,91] 91)
   122.1 --- a/src/HOL/Nitpick.thy	Thu Sep 11 19:26:59 2014 +0200
   122.2 +++ b/src/HOL/Nitpick.thy	Thu Sep 11 19:32:36 2014 +0200
   122.3 @@ -14,9 +14,9 @@
   122.4    "nitpick_params" :: thy_decl
   122.5  begin
   122.6  
   122.7 -datatype_new (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
   122.8 -datatype_new (dead 'a, dead 'b) pair_box = PairBox 'a 'b
   122.9 -datatype_new (dead 'a) word = Word "'a set"
  122.10 +datatype (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
  122.11 +datatype (dead 'a, dead 'b) pair_box = PairBox 'a 'b
  122.12 +datatype (dead 'a) word = Word "'a set"
  122.13  
  122.14  typedecl bisim_iterator
  122.15  typedecl unsigned_bit
   123.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Thu Sep 11 19:26:59 2014 +0200
   123.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Thu Sep 11 19:32:36 2014 +0200
   123.3 @@ -44,7 +44,7 @@
   123.4  nitpick [card = 17, expect = none]
   123.5  oops
   123.6  
   123.7 -datatype_new ('a, 'b) pd = Pd "'a \<times> 'b"
   123.8 +datatype ('a, 'b) pd = Pd "'a \<times> 'b"
   123.9  
  123.10  fun fs where
  123.11  "fs (Pd (a, _)) = a"
  123.12 @@ -76,7 +76,7 @@
  123.13  nitpick [expect = genuine]
  123.14  oops
  123.15  
  123.16 -datatype_new ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
  123.17 +datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
  123.18  
  123.19  fun app where
  123.20  "app (Fn f) x = f x"
   124.1 --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Thu Sep 11 19:26:59 2014 +0200
   124.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Thu Sep 11 19:32:36 2014 +0200
   124.3 @@ -206,7 +206,7 @@
   124.4  nitpick [binary_ints, expect = none]
   124.5  sorry
   124.6  
   124.7 -datatype_new tree = Null | Node nat tree tree
   124.8 +datatype tree = Null | Node nat tree tree
   124.9  
  124.10  primrec labels where
  124.11  "labels Null = {}" |
   125.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Sep 11 19:26:59 2014 +0200
   125.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Sep 11 19:32:36 2014 +0200
   125.3 @@ -223,7 +223,7 @@
   125.4  
   125.5  subsection {* 2.10. Boxing *}
   125.6  
   125.7 -datatype_new tm = Var nat | Lam tm | App tm tm
   125.8 +datatype tm = Var nat | Lam tm | App tm tm
   125.9  
  125.10  primrec lift where
  125.11  "lift (Var j) k = Var (if j < k then j else j + 1)" |
  125.12 @@ -306,7 +306,7 @@
  125.13  
  125.14  subsection {* 3.1. A Context-Free Grammar *}
  125.15  
  125.16 -datatype_new alphabet = a | b
  125.17 +datatype alphabet = a | b
  125.18  
  125.19  inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
  125.20    "[] \<in> S\<^sub>1"
  125.21 @@ -381,7 +381,7 @@
  125.22  
  125.23  subsection {* 3.2. AA Trees *}
  125.24  
  125.25 -datatype_new 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
  125.26 +datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
  125.27  
  125.28  primrec data where
  125.29  "data \<Lambda> = undefined" |
   126.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Thu Sep 11 19:26:59 2014 +0200
   126.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Thu Sep 11 19:32:36 2014 +0200
   126.3 @@ -617,7 +617,7 @@
   126.4  
   126.5  text {* Non-recursive datatypes *}
   126.6  
   126.7 -datatype_new T1 = A | B
   126.8 +datatype T1 = A | B
   126.9  
  126.10  lemma "P (x\<Colon>T1)"
  126.11  nitpick [expect = genuine]
  126.12 @@ -653,7 +653,7 @@
  126.13  nitpick [expect = genuine]
  126.14  oops
  126.15  
  126.16 -datatype_new 'a T2 = C T1 | D 'a
  126.17 +datatype 'a T2 = C T1 | D 'a
  126.18  
  126.19  lemma "P (x\<Colon>'a T2)"
  126.20  nitpick [expect = genuine]
  126.21 @@ -685,7 +685,7 @@
  126.22  nitpick [expect = genuine]
  126.23  oops
  126.24  
  126.25 -datatype_new ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
  126.26 +datatype ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
  126.27  
  126.28  lemma "P (x\<Colon>('a, 'b) T3)"
  126.29  nitpick [expect = genuine]
  126.30 @@ -790,7 +790,7 @@
  126.31  nitpick [expect = genuine]
  126.32  oops
  126.33  
  126.34 -datatype_new BitList = BitListNil | Bit0 BitList | Bit1 BitList
  126.35 +datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
  126.36  
  126.37  lemma "P (x\<Colon>BitList)"
  126.38  nitpick [expect = genuine]
  126.39 @@ -823,7 +823,7 @@
  126.40  nitpick [expect = genuine]
  126.41  oops
  126.42  
  126.43 -datatype_new 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
  126.44 +datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
  126.45  
  126.46  lemma "P (x\<Colon>'a BinTree)"
  126.47  nitpick [expect = genuine]
  126.48 @@ -857,7 +857,7 @@
  126.49  
  126.50  text {* Mutually recursive datatypes *}
  126.51  
  126.52 -datatype_new 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
  126.53 +datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
  126.54   and 'a bexp = Equal "'a aexp" "'a aexp"
  126.55  
  126.56  lemma "P (x\<Colon>'a aexp)"
  126.57 @@ -911,7 +911,7 @@
  126.58  nitpick [expect = genuine]
  126.59  oops
  126.60  
  126.61 -datatype_new X = A | B X | C Y and Y = D X | E Y | F
  126.62 +datatype X = A | B X | C Y and Y = D X | E Y | F
  126.63  
  126.64  lemma "P (x\<Colon>X)"
  126.65  nitpick [expect = genuine]
  126.66 @@ -999,7 +999,7 @@
  126.67  
  126.68  text {* Indirect recursion is implemented via mutual recursion. *}
  126.69  
  126.70 -datatype_new XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
  126.71 +datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
  126.72  
  126.73  lemma "P (x\<Colon>XOpt)"
  126.74  nitpick [expect = genuine]
  126.75 @@ -1017,7 +1017,7 @@
  126.76  nitpick [expect = genuine]
  126.77  oops
  126.78  
  126.79 -datatype_new 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
  126.80 +datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
  126.81  
  126.82  lemma "P (x\<Colon>'a YOpt)"
  126.83  nitpick [expect = genuine]
  126.84 @@ -1031,7 +1031,7 @@
  126.85  nitpick [expect = genuine]
  126.86  oops
  126.87  
  126.88 -datatype_new Trie = TR "Trie list"
  126.89 +datatype Trie = TR "Trie list"
  126.90  
  126.91  lemma "P (x\<Colon>Trie)"
  126.92  nitpick [expect = genuine]
  126.93 @@ -1045,7 +1045,7 @@
  126.94  nitpick [expect = genuine]
  126.95  oops
  126.96  
  126.97 -datatype_new InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
  126.98 +datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
  126.99  
 126.100  lemma "P (x\<Colon>InfTree)"
 126.101  nitpick [expect = genuine]
 126.102 @@ -1073,7 +1073,7 @@
 126.103  nitpick [expect = genuine]
 126.104  oops
 126.105  
 126.106 -datatype_new 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
 126.107 +datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
 126.108  
 126.109  lemma "P (x\<Colon>'a lambda)"
 126.110  nitpick [expect = genuine]
 126.111 @@ -1109,8 +1109,8 @@
 126.112  
 126.113  text {* Taken from "Inductive datatypes in HOL", p. 8: *}
 126.114  
 126.115 -datatype_new (dead 'a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
 126.116 -datatype_new 'c U = E "('c, 'c U) T"
 126.117 +datatype (dead 'a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
 126.118 +datatype 'c U = E "('c, 'c U) T"
 126.119  
 126.120  lemma "P (x\<Colon>'c U)"
 126.121  nitpick [expect = genuine]
   127.1 --- a/src/HOL/Nominal/Examples/CK_Machine.thy	Thu Sep 11 19:26:59 2014 +0200
   127.2 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Thu Sep 11 19:32:36 2014 +0200
   127.3 @@ -81,7 +81,7 @@
   127.4  
   127.5  section {* Evaluation Contexts *}
   127.6  
   127.7 -datatype_new ctx = 
   127.8 +datatype ctx = 
   127.9      Hole ("\<box>")  
  127.10    | CAPPL "ctx" "lam"
  127.11    | CAPPR "lam" "ctx"
   128.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Thu Sep 11 19:26:59 2014 +0200
   128.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Thu Sep 11 19:32:36 2014 +0200
   128.3 @@ -38,7 +38,7 @@
   128.4  where
   128.5    "\<lambda>x:T. t \<equiv> Abs T x t"
   128.6  
   128.7 -datatype_new pat =
   128.8 +datatype pat =
   128.9      PVar name ty
  128.10    | PTuple pat pat  ("(1'\<langle>\<langle>_,/ _'\<rangle>\<rangle>)")
  128.11  
   129.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Sep 11 19:26:59 2014 +0200
   129.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Sep 11 19:32:36 2014 +0200
   129.3 @@ -18,12 +18,12 @@
   129.4    swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
   129.5  
   129.6  (* a "private" copy of the option type used in the abstraction function *)
   129.7 -datatype_new 'a noption = nSome 'a | nNone
   129.8 +datatype 'a noption = nSome 'a | nNone
   129.9  
  129.10  datatype_compat noption
  129.11  
  129.12  (* a "private" copy of the product type used in the nominal induct method *)
  129.13 -datatype_new ('a, 'b) nprod = nPair 'a 'b
  129.14 +datatype ('a, 'b) nprod = nPair 'a 'b
  129.15  
  129.16  datatype_compat nprod
  129.17  
   130.1 --- a/src/HOL/Num.thy	Thu Sep 11 19:26:59 2014 +0200
   130.2 +++ b/src/HOL/Num.thy	Thu Sep 11 19:32:36 2014 +0200
   130.3 @@ -11,7 +11,7 @@
   130.4  
   130.5  subsection {* The @{text num} type *}
   130.6  
   130.7 -datatype_new num = One | Bit0 num | Bit1 num
   130.8 +datatype num = One | Bit0 num | Bit1 num
   130.9  
  130.10  text {* Increment function for type @{typ num} *}
  130.11  
   131.1 --- a/src/HOL/Option.thy	Thu Sep 11 19:26:59 2014 +0200
   131.2 +++ b/src/HOL/Option.thy	Thu Sep 11 19:32:36 2014 +0200
   131.3 @@ -8,7 +8,7 @@
   131.4  imports BNF_Least_Fixpoint Finite_Set
   131.5  begin
   131.6  
   131.7 -datatype_new 'a option =
   131.8 +datatype 'a option =
   131.9      None
  131.10    | Some (the: 'a)
  131.11  
   132.1 --- a/src/HOL/Predicate.thy	Thu Sep 11 19:26:59 2014 +0200
   132.2 +++ b/src/HOL/Predicate.thy	Thu Sep 11 19:32:36 2014 +0200
   132.3 @@ -10,7 +10,7 @@
   132.4  
   132.5  subsection {* The type of predicate enumerations (a monad) *}
   132.6  
   132.7 -datatype_new 'a pred = Pred "'a \<Rightarrow> bool"
   132.8 +datatype 'a pred = Pred "'a \<Rightarrow> bool"
   132.9  
  132.10  primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where
  132.11    eval_pred: "eval (Pred f) = f"
  132.12 @@ -402,7 +402,7 @@
  132.13  
  132.14  subsection {* Implementation *}
  132.15  
  132.16 -datatype_new 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
  132.17 +datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
  132.18  
  132.19  primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
  132.20    "pred_of_seq Empty = \<bottom>"
   133.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
   133.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
   133.3 @@ -107,7 +107,7 @@
   133.4  
   133.5  hide_const Pow
   133.6  
   133.7 -datatype_new expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
   133.8 +datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
   133.9    | Minus expr expr | Uminus expr | Pow expr int | Exp expr
  133.10  
  133.11  text {*
  133.12 @@ -197,7 +197,7 @@
  133.13  
  133.14  section {* Example negation *}
  133.15  
  133.16 -datatype_new abc = A | B | C
  133.17 +datatype abc = A | B | C
  133.18  
  133.19  inductive notB :: "abc => bool"
  133.20  where
   134.1 --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Thu Sep 11 19:26:59 2014 +0200
   134.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Thu Sep 11 19:32:36 2014 +0200
   134.3 @@ -24,7 +24,7 @@
   134.4      (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
   134.5  *}
   134.6  
   134.7 -datatype_new alphabet = a | b
   134.8 +datatype alphabet = a | b
   134.9  
  134.10  inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
  134.11    "[] \<in> S\<^sub>1"
   135.1 --- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Thu Sep 11 19:26:59 2014 +0200
   135.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Thu Sep 11 19:32:36 2014 +0200
   135.3 @@ -10,11 +10,11 @@
   135.4  
   135.5  text {* a contribution by Aditi Barthwal *}
   135.6  
   135.7 -datatype_new ('nts,'ts) symbol = NTS 'nts
   135.8 +datatype ('nts,'ts) symbol = NTS 'nts
   135.9                              | TS 'ts
  135.10  
  135.11                              
  135.12 -datatype_new ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"
  135.13 +datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"
  135.14  
  135.15  type_synonym ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts"
  135.16  
  135.17 @@ -75,7 +75,7 @@
  135.18  
  135.19  subsection {* Some concrete Context Free Grammars *}
  135.20  
  135.21 -datatype_new alphabet = a | b
  135.22 +datatype alphabet = a | b
  135.23  
  135.24  inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
  135.25    "[] \<in> S\<^sub>1"
  135.26 @@ -140,7 +140,7 @@
  135.27  type_synonym var = nat
  135.28  type_synonym state = "int list"
  135.29  
  135.30 -datatype_new com =
  135.31 +datatype com =
  135.32    Skip |
  135.33    Ass var "state => int" |
  135.34    Seq com com |
  135.35 @@ -164,11 +164,11 @@
  135.36  
  135.37  subsection {* Lambda *}
  135.38  
  135.39 -datatype_new type =
  135.40 +datatype type =
  135.41      Atom nat
  135.42    | Fun type type    (infixr "\<Rightarrow>" 200)
  135.43  
  135.44 -datatype_new dB =
  135.45 +datatype dB =
  135.46      Var nat
  135.47    | App dB dB (infixl "\<degree>" 200)
  135.48    | Abs type dB
  135.49 @@ -237,12 +237,12 @@
  135.50  type_synonym vvalue = int
  135.51  type_synonym var_assign = "vname \<Rightarrow> vvalue"  --"variable assignment"
  135.52  
  135.53 -datatype_new ir_expr = 
  135.54 +datatype ir_expr = 
  135.55    IrConst vvalue
  135.56  | ObjAddr vname
  135.57  | Add ir_expr ir_expr
  135.58  
  135.59 -datatype_new val =
  135.60 +datatype val =
  135.61    IntVal  vvalue
  135.62  
  135.63  record  configuration =
  135.64 @@ -267,14 +267,14 @@
  135.65  type_synonym name = nat --"For simplicity in examples"
  135.66  type_synonym state' = "name \<Rightarrow> nat"
  135.67  
  135.68 -datatype_new aexp = N nat | V name | Plus aexp aexp
  135.69 +datatype aexp = N nat | V name | Plus aexp aexp
  135.70  
  135.71  fun aval :: "aexp \<Rightarrow> state' \<Rightarrow> nat" where
  135.72  "aval (N n) _ = n" |
  135.73  "aval (V x) st = st x" |
  135.74  "aval (Plus e\<^sub>1 e\<^sub>2) st = aval e\<^sub>1 st + aval e\<^sub>2 st"
  135.75  
  135.76 -datatype_new bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
  135.77 +datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
  135.78  
  135.79  primrec bval :: "bexp \<Rightarrow> state' \<Rightarrow> bool" where
  135.80  "bval (B b) _ = b" |
  135.81 @@ -282,7 +282,7 @@
  135.82  "bval (And b1 b2) st = (bval b1 st \<and> bval b2 st)" |
  135.83  "bval (Less a\<^sub>1 a\<^sub>2) st = (aval a\<^sub>1 st < aval a\<^sub>2 st)"
  135.84  
  135.85 -datatype_new
  135.86 +datatype
  135.87    com' = SKIP 
  135.88        | Assign name aexp         ("_ ::= _" [1000, 61] 61)
  135.89        | Semi   com'  com'          ("_; _"  [60, 61] 60)
  135.90 @@ -326,7 +326,7 @@
  135.91  text{* This example formalizes finite CCS processes without communication or
  135.92  recursion. For simplicity, labels are natural numbers. *}
  135.93  
  135.94 -datatype_new proc = nil | pre nat proc | or proc proc | par proc proc
  135.95 +datatype proc = nil | pre nat proc | or proc proc | par proc proc
  135.96  
  135.97  inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
  135.98  "step (pre n p) n p" |
   136.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Thu Sep 11 19:26:59 2014 +0200
   136.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Thu Sep 11 19:32:36 2014 +0200
   136.3 @@ -2,13 +2,13 @@
   136.4  imports Main
   136.5  begin
   136.6  
   136.7 -datatype_new guest = Guest0 | Guest1
   136.8 -datatype_new key = Key0 | Key1 | Key2 | Key3
   136.9 -datatype_new room = Room0
  136.10 +datatype guest = Guest0 | Guest1
  136.11 +datatype key = Key0 | Key1 | Key2 | Key3
  136.12 +datatype room = Room0
  136.13  
  136.14  type_synonym card = "key * key"
  136.15  
  136.16 -datatype_new event =
  136.17 +datatype event =
  136.18     Check_in guest room card | Enter guest room card | Exit guest room
  136.19  
  136.20  definition initk :: "room \<Rightarrow> key"
   137.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Thu Sep 11 19:26:59 2014 +0200
   137.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Thu Sep 11 19:32:36 2014 +0200
   137.3 @@ -11,7 +11,7 @@
   137.4  type_synonym var = unit
   137.5  type_synonym state = bool
   137.6  
   137.7 -datatype_new com =
   137.8 +datatype com =
   137.9    Skip |
  137.10    Ass bool |
  137.11    Seq com com |
   138.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Thu Sep 11 19:26:59 2014 +0200
   138.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Thu Sep 11 19:32:36 2014 +0200
   138.3 @@ -11,7 +11,7 @@
   138.4  type_synonym var = unit
   138.5  type_synonym state = bool
   138.6  
   138.7 -datatype_new com =
   138.8 +datatype com =
   138.9    Skip |
  138.10    Ass bool |
  138.11    Seq com com |
   139.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Thu Sep 11 19:26:59 2014 +0200
   139.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Thu Sep 11 19:32:36 2014 +0200
   139.3 @@ -11,7 +11,7 @@
   139.4  type_synonym var = unit
   139.5  type_synonym state = int
   139.6  
   139.7 -datatype_new com =
   139.8 +datatype com =
   139.9    Skip |
  139.10    Ass var "int" |
  139.11    Seq com com |
   140.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Thu Sep 11 19:26:59 2014 +0200
   140.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Thu Sep 11 19:32:36 2014 +0200
   140.3 @@ -11,7 +11,7 @@
   140.4  type_synonym var = nat
   140.5  type_synonym state = "int list"
   140.6  
   140.7 -datatype_new com =
   140.8 +datatype com =
   140.9    Skip |
  140.10    Ass var "int" |
  140.11    Seq com com |
   141.1 --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Thu Sep 11 19:26:59 2014 +0200
   141.2 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Thu Sep 11 19:32:36 2014 +0200
   141.3 @@ -4,11 +4,11 @@
   141.4  
   141.5  subsection {* Lambda *}
   141.6  
   141.7 -datatype_new type =
   141.8 +datatype type =
   141.9      Atom nat
  141.10    | Fun type type    (infixr "\<Rightarrow>" 200)
  141.11  
  141.12 -datatype_new dB =
  141.13 +datatype dB =
  141.14      Var nat
  141.15    | App dB dB (infixl "\<degree>" 200)
  141.16    | Abs type dB
   142.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
   142.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
   142.3 @@ -53,7 +53,7 @@
   142.4  
   142.5  section {* Context Free Grammar *}
   142.6  
   142.7 -datatype_new alphabet = a | b
   142.8 +datatype alphabet = a | b
   142.9  
  142.10  inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
  142.11    "[] \<in> S\<^sub>1"
  142.12 @@ -179,7 +179,7 @@
  142.13  type_synonym var = nat
  142.14  type_synonym state = "int list"
  142.15  
  142.16 -datatype_new com =
  142.17 +datatype com =
  142.18    Skip |
  142.19    Ass var "int" |
  142.20    Seq com com |
  142.21 @@ -206,11 +206,11 @@
  142.22  
  142.23  subsection {* Lambda *}
  142.24  
  142.25 -datatype_new type =
  142.26 +datatype type =
  142.27      Atom nat
  142.28    | Fun type type    (infixr "\<Rightarrow>" 200)
  142.29  
  142.30 -datatype_new dB =
  142.31 +datatype dB =
  142.32      Var nat
  142.33    | App dB dB (infixl "\<degree>" 200)
  142.34    | Abs type dB
   143.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Sep 11 19:26:59 2014 +0200
   143.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Sep 11 19:32:36 2014 +0200
   143.3 @@ -139,7 +139,7 @@
   143.4  
   143.5  subsection {* Alternative Rules *}
   143.6  
   143.7 -datatype_new char = C | D | E | F | G | H
   143.8 +datatype char = C | D | E | F | G | H
   143.9  
  143.10  inductive is_C_or_D
  143.11  where
  143.12 @@ -784,7 +784,7 @@
  143.13  type_synonym var = nat
  143.14  type_synonym state = "int list"
  143.15  
  143.16 -datatype_new com =
  143.17 +datatype com =
  143.18    Skip |
  143.19    Ass var "state => int" |
  143.20    Seq com com |
  143.21 @@ -809,7 +809,7 @@
  143.22  text{* This example formalizes finite CCS processes without communication or
  143.23  recursion. For simplicity, labels are natural numbers. *}
  143.24  
  143.25 -datatype_new proc = nil | pre nat proc | or proc proc | par proc proc
  143.26 +datatype proc = nil | pre nat proc | or proc proc | par proc proc
  143.27  
  143.28  inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
  143.29  where
  143.30 @@ -974,7 +974,7 @@
  143.31  *)
  143.32  subsection {* AVL Tree *}
  143.33  
  143.34 -datatype_new 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
  143.35 +datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
  143.36  fun height :: "'a tree => nat" where
  143.37  "height ET = 0"
  143.38  | "height (MKT x l r h) = max (height l) (height r) + 1"
  143.39 @@ -1403,7 +1403,7 @@
  143.40  
  143.41  thm is_error'.equation
  143.42  
  143.43 -datatype_new ErrorObject = Error String.literal int
  143.44 +datatype ErrorObject = Error String.literal int
  143.45  
  143.46  inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
  143.47  where
  143.48 @@ -1508,7 +1508,7 @@
  143.49  
  143.50  text {* The higher-order predicate r is in an output term *}
  143.51  
  143.52 -datatype_new result = Result bool
  143.53 +datatype result = Result bool
  143.54  
  143.55  inductive fixed_relation :: "'a => bool"
  143.56  
   144.1 --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Thu Sep 11 19:26:59 2014 +0200
   144.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Thu Sep 11 19:32:36 2014 +0200
   144.3 @@ -9,7 +9,7 @@
   144.4    manually slightly adapted.
   144.5  *}
   144.6   
   144.7 -datatype_new Nat = Zer
   144.8 +datatype Nat = Zer
   144.9               | Suc Nat
  144.10  
  144.11  fun sub :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat"
  144.12 @@ -20,10 +20,10 @@
  144.13                                           Zer \<Rightarrow> Zer
  144.14                                         | Suc x' \<Rightarrow> sub x' y')"
  144.15  
  144.16 -datatype_new Sym = N0
  144.17 +datatype Sym = N0
  144.18               | N1 Sym
  144.19  
  144.20 -datatype_new RE = Sym Sym
  144.21 +datatype RE = Sym Sym
  144.22              | Or RE RE
  144.23              | Seq RE RE
  144.24              | And RE RE
   145.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
   145.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
   145.3 @@ -107,13 +107,13 @@
   145.4    "unique [] = True"
   145.5  | "unique (x # xs) = (xs\<langle>fst x\<rangle>\<^sub>? = \<bottom> \<and> unique xs)"
   145.6  
   145.7 -datatype_new type =
   145.8 +datatype type =
   145.9      TVar nat
  145.10    | Top
  145.11    | Fun type type    (infixr "\<rightarrow>" 200)
  145.12    | TyAll type type  ("(3\<forall><:_./ _)" [0, 10] 10)
  145.13  
  145.14 -datatype_new binding = VarB type | TVarB type
  145.15 +datatype binding = VarB type | TVarB type
  145.16  type_synonym env = "binding list"
  145.17  
  145.18  primrec is_TVarB :: "binding \<Rightarrow> bool"
  145.19 @@ -131,7 +131,7 @@
  145.20    "mapB f (VarB T) = VarB (f T)"
  145.21  | "mapB f (TVarB T) = TVarB (f T)"
  145.22  
  145.23 -datatype_new trm =
  145.24 +datatype trm =
  145.25      Var nat
  145.26    | Abs type trm   ("(3\<lambda>:_./ _)" [0, 10] 10)
  145.27    | TAbs type trm  ("(3\<lambda><:_./ _)" [0, 10] 10)
   146.1 --- a/src/HOL/Proofs/Extraction/Higman.thy	Thu Sep 11 19:26:59 2014 +0200
   146.2 +++ b/src/HOL/Proofs/Extraction/Higman.thy	Thu Sep 11 19:32:36 2014 +0200
   146.3 @@ -14,7 +14,7 @@
   146.4    based on Coquand and Fridlender \cite{Coquand93}.
   146.5  *}
   146.6  
   146.7 -datatype_new letter = A | B
   146.8 +datatype letter = A | B
   146.9  
  146.10  inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"
  146.11  where
   147.1 --- a/src/HOL/Proofs/Extraction/Warshall.thy	Thu Sep 11 19:26:59 2014 +0200
   147.2 +++ b/src/HOL/Proofs/Extraction/Warshall.thy	Thu Sep 11 19:32:36 2014 +0200
   147.3 @@ -13,7 +13,7 @@
   147.4    based on Berger, Schwichtenberg and Seisenberger \cite{Berger-JAR-2001}.
   147.5  *}
   147.6  
   147.7 -datatype_new b = T | F
   147.8 +datatype b = T | F
   147.9  
  147.10  primrec
  147.11    is_path' :: "('a \<Rightarrow> 'a \<Rightarrow> b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
   148.1 --- a/src/HOL/Proofs/Lambda/Lambda.thy	Thu Sep 11 19:26:59 2014 +0200
   148.2 +++ b/src/HOL/Proofs/Lambda/Lambda.thy	Thu Sep 11 19:32:36 2014 +0200
   148.3 @@ -12,7 +12,7 @@
   148.4  
   148.5  subsection {* Lambda-terms in de Bruijn notation and substitution *}
   148.6  
   148.7 -datatype_new dB =
   148.8 +datatype dB =
   148.9      Var nat
  148.10    | App dB dB (infixl "\<degree>" 200)
  148.11    | Abs dB
   149.1 --- a/src/HOL/Proofs/Lambda/LambdaType.thy	Thu Sep 11 19:26:59 2014 +0200
   149.2 +++ b/src/HOL/Proofs/Lambda/LambdaType.thy	Thu Sep 11 19:32:36 2014 +0200
   149.3 @@ -35,7 +35,7 @@
   149.4  
   149.5  subsection {* Types and typing rules *}
   149.6  
   149.7 -datatype_new type =
   149.8 +datatype type =
   149.9      Atom nat
  149.10    | Fun type type    (infixr "\<Rightarrow>" 200)
  149.11  
   150.1 --- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Thu Sep 11 19:26:59 2014 +0200
   150.2 +++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Thu Sep 11 19:32:36 2014 +0200
   150.3 @@ -2,7 +2,7 @@
   150.4  imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
   150.5  begin
   150.6  
   150.7 -datatype_new agent = Alice | Bob | Spy
   150.8 +datatype agent = Alice | Bob | Spy
   150.9  
  150.10  definition agents :: "agent set"
  150.11  where
  150.12 @@ -12,14 +12,14 @@
  150.13  where
  150.14    "bad = {Spy}"
  150.15  
  150.16 -datatype_new key = pubEK agent | priEK agent
  150.17 +datatype key = pubEK agent | priEK agent
  150.18  
  150.19  fun invKey
  150.20  where
  150.21    "invKey (pubEK A) = priEK A"
  150.22  | "invKey (priEK A) = pubEK A"
  150.23  
  150.24 -datatype_new
  150.25 +datatype
  150.26       msg = Agent  agent
  150.27           | Key    key
  150.28           | Nonce  nat
  150.29 @@ -73,7 +73,7 @@
  150.30  | initState_Spy:
  150.31      "initState Spy        =  (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)"
  150.32  
  150.33 -datatype_new
  150.34 +datatype
  150.35    event = Says  agent agent msg
  150.36          | Gets  agent       msg
  150.37          | Notes agent       msg
   151.1 --- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Thu Sep 11 19:26:59 2014 +0200
   151.2 +++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Thu Sep 11 19:32:36 2014 +0200
   151.3 @@ -2,13 +2,13 @@
   151.4  imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
   151.5  begin
   151.6  
   151.7 -datatype_new guest = Guest0 | Guest1
   151.8 -datatype_new key = Key0 | Key1 | Key2 | Key3
   151.9 -datatype_new room = Room0
  151.10 +datatype guest = Guest0 | Guest1
  151.11 +datatype key = Key0 | Key1 | Key2 | Key3
  151.12 +datatype room = Room0
  151.13  
  151.14  type_synonym card = "key * key"
  151.15  
  151.16 -datatype_new event =
  151.17 +datatype event =
  151.18    Check_in guest room card
  151.19  | Enter guest room card
  151.20  | Exit guest room
   152.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
   152.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
   152.3 @@ -122,7 +122,7 @@
   152.4  
   152.5  subsection {* Trees *}
   152.6  
   152.7 -datatype_new 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
   152.8 +datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
   152.9  
  152.10  primrec leaves :: "'a tree \<Rightarrow> 'a list" where
  152.11    "leaves Twig = []"
  152.12 @@ -150,7 +150,7 @@
  152.13      --{* Wrong! *} 
  152.14    oops
  152.15  
  152.16 -datatype_new 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
  152.17 +datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
  152.18  
  152.19  primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
  152.20    "inOrder (Tip a)= [a]"
  152.21 @@ -439,7 +439,7 @@
  152.22  quickcheck[random, expect = counterexample]
  152.23  oops
  152.24  
  152.25 -datatype_new colour = Red | Green | Blue
  152.26 +datatype colour = Red | Green | Blue
  152.27  
  152.28  record cpoint = point +
  152.29    colour :: colour
   153.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
   153.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
   153.3 @@ -132,7 +132,7 @@
   153.4  
   153.5  subsection {* AVL Trees *}
   153.6  
   153.7 -datatype_new 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
   153.8 +datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
   153.9  
  153.10  primrec set_of :: "'a tree \<Rightarrow> 'a set"
  153.11  where
   154.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Sep 11 19:26:59 2014 +0200
   154.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Sep 11 19:32:36 2014 +0200
   154.3 @@ -574,8 +574,8 @@
   154.4  where
   154.5    "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
   154.6  
   154.7 -datatype_new (dead 'a) unknown = Unknown | Known 'a
   154.8 -datatype_new (dead 'a) three_valued = Unknown_value | Value 'a | No_value
   154.9 +datatype (dead 'a) unknown = Unknown | Known 'a
  154.10 +datatype (dead 'a) three_valued = Unknown_value | Value 'a | No_value
  154.11  
  154.12  type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued"
  154.13  
   155.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Sep 11 19:26:59 2014 +0200
   155.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Sep 11 19:32:36 2014 +0200
   155.3 @@ -26,14 +26,14 @@
   155.4  
   155.5  subsubsection {* Narrowing's deep representation of types and terms *}
   155.6  
   155.7 -datatype_new narrowing_type =
   155.8 +datatype narrowing_type =
   155.9    Narrowing_sum_of_products "narrowing_type list list"
  155.10  
  155.11 -datatype_new narrowing_term =
  155.12 +datatype narrowing_term =
  155.13    Narrowing_variable "integer list" narrowing_type
  155.14  | Narrowing_constructor integer "narrowing_term list"
  155.15  
  155.16 -datatype_new (dead 'a) narrowing_cons =
  155.17 +datatype (dead 'a) narrowing_cons =
  155.18    Narrowing_cons narrowing_type "(narrowing_term list \<Rightarrow> 'a) list"
  155.19  
  155.20  primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
  155.21 @@ -127,7 +127,7 @@
  155.22  class narrowing =
  155.23    fixes narrowing :: "integer => 'a narrowing_cons"
  155.24  
  155.25 -datatype_new property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
  155.26 +datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
  155.27  
  155.28  (* FIXME: hard-wired maximal depth of 100 here *)
  155.29  definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
  155.30 @@ -155,7 +155,7 @@
  155.31  
  155.32  subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
  155.33  
  155.34 -datatype_new (dead 'a, dead 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
  155.35 +datatype (dead 'a, dead 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
  155.36  
  155.37  primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b"
  155.38  where
  155.39 @@ -165,7 +165,7 @@
  155.40  hide_type (open) ffun
  155.41  hide_const (open) Constant Update eval_ffun
  155.42  
  155.43 -datatype_new (dead 'b) cfun = Constant 'b
  155.44 +datatype (dead 'b) cfun = Constant 'b
  155.45  
  155.46  primrec eval_cfun :: "'b cfun => 'a => 'b"
  155.47  where
   156.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Thu Sep 11 19:26:59 2014 +0200
   156.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Thu Sep 11 19:32:36 2014 +0200
   156.3 @@ -10,7 +10,7 @@
   156.4  
   156.5  subsection{*Defining the Free Algebra*}
   156.6  
   156.7 -datatype_new
   156.8 +datatype
   156.9    freemsg = NONCE  nat
  156.10          | MPAIR  freemsg freemsg
  156.11          | CRYPT  nat freemsg
   157.1 --- a/src/HOL/Record.thy	Thu Sep 11 19:26:59 2014 +0200
   157.2 +++ b/src/HOL/Record.thy	Thu Sep 11 19:32:36 2014 +0200
   157.3 @@ -79,7 +79,7 @@
   157.4  
   157.5  subsection {* Operators and lemmas for types isomorphic to tuples *}
   157.6  
   157.7 -datatype_new (dead 'a, dead 'b, dead 'c) tuple_isomorphism =
   157.8 +datatype (dead 'a, dead 'b, dead 'c) tuple_isomorphism =
   157.9    Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
  157.10  
  157.11  primrec
   158.1 --- a/src/HOL/SET_Protocol/Event_SET.thy	Thu Sep 11 19:26:59 2014 +0200
   158.2 +++ b/src/HOL/SET_Protocol/Event_SET.thy	Thu Sep 11 19:32:36 2014 +0200
   158.3 @@ -15,7 +15,7 @@
   158.4  
   158.5  
   158.6  text{*Message events*}
   158.7 -datatype_new
   158.8 +datatype
   158.9    event = Says  agent agent msg
  158.10          | Gets  agent       msg
  158.11          | Notes agent       msg
   159.1 --- a/src/HOL/SET_Protocol/Message_SET.thy	Thu Sep 11 19:26:59 2014 +0200
   159.2 +++ b/src/HOL/SET_Protocol/Message_SET.thy	Thu Sep 11 19:32:36 2014 +0200
   159.3 @@ -52,11 +52,11 @@
   159.4  
   159.5  text{*Agents. We allow any number of certification authorities, cardholders
   159.6              merchants, and payment gateways.*}
   159.7 -datatype_new
   159.8 +datatype
   159.9    agent = CA nat | Cardholder nat | Merchant nat | PG nat | Spy
  159.10  
  159.11  text{*Messages*}
  159.12 -datatype_new
  159.13 +datatype
  159.14       msg = Agent  agent     --{*Agent names*}
  159.15           | Number nat       --{*Ordinary integers, timestamps, ...*}
  159.16           | Nonce  nat       --{*Unguessable nonces*}
   160.1 --- a/src/HOL/SPARK/Manual/Complex_Types.thy	Thu Sep 11 19:26:59 2014 +0200
   160.2 +++ b/src/HOL/SPARK/Manual/Complex_Types.thy	Thu Sep 11 19:32:36 2014 +0200
   160.3 @@ -2,7 +2,7 @@
   160.4  imports "../SPARK"
   160.5  begin
   160.6  
   160.7 -datatype_new day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
   160.8 +datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
   160.9  
  160.10  record two_fields =
  160.11    Field1 :: "int \<times> day \<Rightarrow> int"
   161.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Thu Sep 11 19:26:59 2014 +0200
   161.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Thu Sep 11 19:32:36 2014 +0200
   161.3 @@ -18,7 +18,7 @@
   161.4  
   161.5  subsection {* The Binary Tree *}
   161.6  
   161.7 -datatype_new 'a tree = Node "'a tree" 'a bool "'a tree" | Tip
   161.8 +datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip
   161.9  
  161.10  
  161.11  text {* The boolean flag in the node marks the content of the node as
   162.1 --- a/src/HOL/String.thy	Thu Sep 11 19:26:59 2014 +0200
   162.2 +++ b/src/HOL/String.thy	Thu Sep 11 19:32:36 2014 +0200
   162.3 @@ -8,7 +8,7 @@
   162.4  
   162.5  subsection {* Characters and strings *}
   162.6  
   162.7 -datatype_new nibble =
   162.8 +datatype nibble =
   162.9      Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
  162.10    | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
  162.11  
  162.12 @@ -114,7 +114,7 @@
  162.13    "nibble_of_nat (n mod 16) = nibble_of_nat n"
  162.14    by (simp add: nibble_of_nat_def)
  162.15  
  162.16 -datatype_new char = Char nibble nibble
  162.17 +datatype char = Char nibble nibble
  162.18    -- "Note: canonical order of character encoding coincides with standard term ordering"
  162.19  
  162.20  syntax
   163.1 --- a/src/HOL/TLA/Inc/Inc.thy	Thu Sep 11 19:26:59 2014 +0200
   163.2 +++ b/src/HOL/TLA/Inc/Inc.thy	Thu Sep 11 19:32:36 2014 +0200
   163.3 @@ -9,7 +9,7 @@
   163.4  begin
   163.5  
   163.6  (* program counter as an enumeration type *)
   163.7 -datatype_new pcount = a | b | g
   163.8 +datatype pcount = a | b | g
   163.9  
  163.10  axiomatization
  163.11    (* program variables *)
   164.1 --- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Thu Sep 11 19:26:59 2014 +0200
   164.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Thu Sep 11 19:32:36 2014 +0200
   164.3 @@ -8,7 +8,7 @@
   164.4  imports RPCParameters
   164.5  begin
   164.6  
   164.7 -datatype_new mClkState = clkA | clkB
   164.8 +datatype mClkState = clkA | clkB
   164.9  
  164.10  (* types sent on the clerk's send and receive channels are argument types
  164.11     of the memory and the RPC, respectively *)
   165.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Thu Sep 11 19:26:59 2014 +0200
   165.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Thu Sep 11 19:32:36 2014 +0200
   165.3 @@ -8,7 +8,7 @@
   165.4  imports Memory RPC MemClerk
   165.5  begin
   165.6  
   165.7 -datatype_new histState = histA | histB
   165.8 +datatype histState = histA | histB
   165.9  
  165.10  type_synonym histType = "(PrIds => histState) stfun"  (* the type of the history variable *)
  165.11  
   166.1 --- a/src/HOL/TLA/Memory/MemoryParameters.thy	Thu Sep 11 19:26:59 2014 +0200
   166.2 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Thu Sep 11 19:32:36 2014 +0200
   166.3 @@ -9,7 +9,7 @@
   166.4  begin
   166.5  
   166.6  (* the memory operations *)
   166.7 -datatype_new memOp = read Locs | "write" Locs Vals
   166.8 +datatype memOp = read Locs | "write" Locs Vals
   166.9  
  166.10  consts
  166.11    (* memory locations and contents *)
   167.1 --- a/src/HOL/TLA/Memory/RPCParameters.thy	Thu Sep 11 19:26:59 2014 +0200
   167.2 +++ b/src/HOL/TLA/Memory/RPCParameters.thy	Thu Sep 11 19:32:36 2014 +0200
   167.3 @@ -13,8 +13,8 @@
   167.4    memory implementation.
   167.5  *)
   167.6  
   167.7 -datatype_new rpcOp = memcall memOp | othercall Vals
   167.8 -datatype_new rpcState = rpcA | rpcB
   167.9 +datatype rpcOp = memcall memOp | othercall Vals
  167.10 +datatype rpcState = rpcA | rpcB
  167.11  
  167.12  consts
  167.13    (* some particular return values *)
   168.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Thu Sep 11 19:26:59 2014 +0200
   168.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Thu Sep 11 19:32:36 2014 +0200
   168.3 @@ -341,7 +341,7 @@
   168.4      fun not_co_datatype (T as Type (s, _)) =
   168.5          if fp = Least_FP andalso
   168.6             is_some (Old_Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then
   168.7 -          error (qsoty T ^ " is not a new-style datatype (cf. \"datatype_new\")")
   168.8 +          error (qsoty T ^ " is not a new-style datatype (cf. \"datatype\")")
   168.9          else
  168.10            not_co_datatype0 T
  168.11        | not_co_datatype T = not_co_datatype0 T;
   169.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 11 19:26:59 2014 +0200
   169.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 11 19:32:36 2014 +0200
   169.3 @@ -1818,7 +1818,7 @@
   169.4      (parse_co_datatype_cmd Least_FP construct_lfp);
   169.5  
   169.6  val _ =
   169.7 -  Outer_Syntax.local_theory @{command_spec "datatype_new"} "define inductive datatypes"
   169.8 +  Outer_Syntax.local_theory @{command_spec "datatype"} "define inductive datatypes"
   169.9      (parse_co_datatype_cmd Least_FP construct_lfp);
  169.10  
  169.11  val _ = Theory.setup (fp_antiquote_setup @{binding datatype});
   170.1 --- a/src/HOL/Typerep.thy	Thu Sep 11 19:26:59 2014 +0200
   170.2 +++ b/src/HOL/Typerep.thy	Thu Sep 11 19:32:36 2014 +0200
   170.3 @@ -6,7 +6,7 @@
   170.4  imports String
   170.5  begin
   170.6  
   170.7 -datatype_new typerep = Typerep String.literal "typerep list"
   170.8 +datatype typerep = Typerep String.literal "typerep list"
   170.9  
  170.10  class typerep =
  170.11    fixes typerep :: "'a itself \<Rightarrow> typerep"
   171.1 --- a/src/HOL/UNITY/Comp/Counter.thy	Thu Sep 11 19:26:59 2014 +0200
   171.2 +++ b/src/HOL/UNITY/Comp/Counter.thy	Thu Sep 11 19:32:36 2014 +0200
   171.3 @@ -13,7 +13,7 @@
   171.4  theory Counter imports "../UNITY_Main" begin
   171.5  
   171.6  (* Variables are names *)
   171.7 -datatype_new name = C | c nat
   171.8 +datatype name = C | c nat
   171.9  type_synonym state = "name=>int"
  171.10  
  171.11  primrec sum  :: "[nat,state]=>int" where
   172.1 --- a/src/HOL/UNITY/Simple/Network.thy	Thu Sep 11 19:26:59 2014 +0200
   172.2 +++ b/src/HOL/UNITY/Simple/Network.thy	Thu Sep 11 19:32:36 2014 +0200
   172.3 @@ -11,9 +11,9 @@
   172.4  
   172.5  (*The state assigns a number to each process variable*)
   172.6  
   172.7 -datatype_new pvar = Sent | Rcvd | Idle
   172.8 +datatype pvar = Sent | Rcvd | Idle
   172.9  
  172.10 -datatype_new pname = Aproc | Bproc
  172.11 +datatype pname = Aproc | Bproc
  172.12  
  172.13  type_synonym state = "pname * pvar => nat"
  172.14  
   173.1 --- a/src/HOL/UNITY/Simple/Token.thy	Thu Sep 11 19:26:59 2014 +0200
   173.2 +++ b/src/HOL/UNITY/Simple/Token.thy	Thu Sep 11 19:32:36 2014 +0200
   173.3 @@ -15,7 +15,7 @@
   173.4  
   173.5  subsection{*Definitions*}
   173.6  
   173.7 -datatype_new pstate = Hungry | Eating | Thinking
   173.8 +datatype pstate = Hungry | Eating | Thinking
   173.9      --{*process states*}
  173.10  
  173.11  record state =
   174.1 --- a/src/HOL/Unix/Nested_Environment.thy	Thu Sep 11 19:26:59 2014 +0200
   174.2 +++ b/src/HOL/Unix/Nested_Environment.thy	Thu Sep 11 19:32:36 2014 +0200
   174.3 @@ -19,7 +19,7 @@
   174.4    position within the structure.
   174.5  *}
   174.6  
   174.7 -datatype_new (dead 'a, dead 'b, dead 'c) env =
   174.8 +datatype (dead 'a, dead 'b, dead 'c) env =
   174.9      Val 'a
  174.10    | Env 'b  "'c \<Rightarrow> ('a, 'b, 'c) env option"
  174.11  
   175.1 --- a/src/HOL/Unix/Unix.thy	Thu Sep 11 19:26:59 2014 +0200
   175.2 +++ b/src/HOL/Unix/Unix.thy	Thu Sep 11 19:32:36 2014 +0200
   175.3 @@ -73,7 +73,7 @@
   175.4    \cite{Naraschewski:2001}.}
   175.5  *}
   175.6  
   175.7 -datatype_new perm =
   175.8 +datatype perm =
   175.9      Readable
  175.10    | Writable
  175.11    | Executable    -- "(ignored)"
  175.12 @@ -284,7 +284,7 @@
  175.13    @{text "root \<midarrow>x\<rightarrow> root'"} for the operational semantics.
  175.14  *}
  175.15  
  175.16 -datatype_new operation =
  175.17 +datatype operation =
  175.18      Read uid string path
  175.19    | Write uid string path
  175.20    | Chmod uid perms path
   176.1 --- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
   176.2 +++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
   176.3 @@ -19,7 +19,7 @@
   176.4  subsection {* Plain Ad Hoc Overloading *}
   176.5  
   176.6  text {*Consider the type of first-order terms.*}
   176.7 -datatype_new ('a, 'b) "term" =
   176.8 +datatype ('a, 'b) "term" =
   176.9    Var 'b |
  176.10    Fun 'a "('a, 'b) term list"
  176.11  
   177.1 --- a/src/HOL/ex/BT.thy	Thu Sep 11 19:26:59 2014 +0200
   177.2 +++ b/src/HOL/ex/BT.thy	Thu Sep 11 19:32:36 2014 +0200
   177.3 @@ -9,7 +9,7 @@
   177.4  
   177.5  theory BT imports Main begin
   177.6  
   177.7 -datatype_new 'a bt =
   177.8 +datatype 'a bt =
   177.9      Lf
  177.10    | Br 'a  "'a bt"  "'a bt"
  177.11  
   178.1 --- a/src/HOL/ex/Chinese.thy	Thu Sep 11 19:26:59 2014 +0200
   178.2 +++ b/src/HOL/ex/Chinese.thy	Thu Sep 11 19:32:36 2014 +0200
   178.3 @@ -16,7 +16,7 @@
   178.4  
   178.5      *}
   178.6  
   178.7 -datatype_new shuzi =
   178.8 +datatype shuzi =
   178.9      One   ("一")
  178.10    | Two   ("二")
  178.11    | Three ("三") 
   179.1 --- a/src/HOL/ex/Eval_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
   179.2 +++ b/src/HOL/ex/Eval_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
   179.3 @@ -42,7 +42,7 @@
   179.4  
   179.5  text {* a fancy datatype *}
   179.6  
   179.7 -datatype_new ('a, 'b) foo =
   179.8 +datatype ('a, 'b) foo =
   179.9      Foo "'a\<Colon>order" 'b
  179.10    | Bla "('a, 'b) bar"
  179.11    | Dummy nat
   180.1 --- a/src/HOL/ex/Fundefs.thy	Thu Sep 11 19:26:59 2014 +0200
   180.2 +++ b/src/HOL/ex/Fundefs.thy	Thu Sep 11 19:32:36 2014 +0200
   180.3 @@ -372,7 +372,7 @@
   180.4  
   180.5  
   180.6  (* Simple Higher-Order Recursion *)
   180.7 -datatype_new 'a tree = 
   180.8 +datatype 'a tree = 
   180.9    Leaf 'a 
  180.10    | Branch "'a tree list"
  180.11  
  180.12 @@ -423,7 +423,7 @@
  180.13  
  180.14  
  180.15  (* Many equations (quadratic blowup) *)
  180.16 -datatype_new DT = 
  180.17 +datatype DT = 
  180.18    A | B | C | D | E | F | G | H | I | J | K | L | M | N | P
  180.19  | Q | R | S | T | U | V
  180.20  
   181.1 --- a/src/HOL/ex/Hebrew.thy	Thu Sep 11 19:26:59 2014 +0200
   181.2 +++ b/src/HOL/ex/Hebrew.thy	Thu Sep 11 19:32:36 2014 +0200
   181.3 @@ -12,7 +12,7 @@
   181.4  
   181.5  text {* The Hebrew Alef-Bet (א-ב). *}
   181.6  
   181.7 -datatype_new alef_bet =
   181.8 +datatype alef_bet =
   181.9      Alef    ("א")
  181.10    | Bet     ("ב")
  181.11    | Gimel   ("ג")
   182.1 --- a/src/HOL/ex/Normalization_by_Evaluation.thy	Thu Sep 11 19:26:59 2014 +0200
   182.2 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Thu Sep 11 19:32:36 2014 +0200
   182.3 @@ -15,7 +15,7 @@
   182.4  lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
   182.5  lemma "~((0::nat) < (0::nat))" by normalization
   182.6  
   182.7 -datatype_new n = Z | S n
   182.8 +datatype n = Z | S n
   182.9  
  182.10  primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where
  182.11     "add Z = id"
   183.1 --- a/src/HOL/ex/Records.thy	Thu Sep 11 19:26:59 2014 +0200
   183.2 +++ b/src/HOL/ex/Records.thy	Thu Sep 11 19:32:36 2014 +0200
   183.3 @@ -166,7 +166,7 @@
   183.4  
   183.5  subsection {* Coloured points: record extension *}
   183.6  
   183.7 -datatype_new colour = Red | Green | Blue
   183.8 +datatype colour = Red | Green | Blue
   183.9  
  183.10  record cpoint = point +
  183.11    colour :: colour
   184.1 --- a/src/HOL/ex/Reflection_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
   184.2 +++ b/src/HOL/ex/Reflection_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
   184.3 @@ -46,7 +46,7 @@
   184.4  text {* Example 1 : Propositional formulae and NNF. *}
   184.5  text {* The type @{text fm} represents simple propositional formulae: *}
   184.6  
   184.7 -datatype_new form = TrueF | FalseF | Less nat nat
   184.8 +datatype form = TrueF | FalseF | Less nat nat
   184.9    | And form form | Or form form | Neg form | ExQ form
  184.10  
  184.11  primrec interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool"
  184.12 @@ -66,7 +66,7 @@
  184.13    apply reify
  184.14    oops
  184.15  
  184.16 -datatype_new fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
  184.17 +datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
  184.18  
  184.19  primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
  184.20  where
  184.21 @@ -135,7 +135,7 @@
  184.22  text {* Example 2: Simple arithmetic formulae *}
  184.23  
  184.24  text {* The type @{text num} reflects linear expressions over natural number *}
  184.25 -datatype_new num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
  184.26 +datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
  184.27  
  184.28  text {* This is just technical to make recursive definitions easier. *}
  184.29  primrec num_size :: "num \<Rightarrow> nat" 
  184.30 @@ -252,7 +252,7 @@
  184.31  
  184.32  text {* Let's lift this to formulae and see what happens *}
  184.33  
  184.34 -datatype_new aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
  184.35 +datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
  184.36    Conj aform aform | Disj aform aform | NEG aform | T | F
  184.37  
  184.38  primrec linaformsize:: "aform \<Rightarrow> nat"
  184.39 @@ -331,7 +331,7 @@
  184.40    one envornement of different types and show that automatic reification also deals with
  184.41    bindings *}
  184.42    
  184.43 -datatype_new rb = BC bool | BAnd rb rb | BOr rb rb
  184.44 +datatype rb = BC bool | BAnd rb rb | BOr rb rb
  184.45  
  184.46  primrec Irb :: "rb \<Rightarrow> bool"
  184.47  where
  184.48 @@ -343,7 +343,7 @@
  184.49    apply (reify Irb.simps)
  184.50  oops
  184.51  
  184.52 -datatype_new rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
  184.53 +datatype rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
  184.54    | INeg rint | ISub rint rint
  184.55  
  184.56  primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
  184.57 @@ -370,7 +370,7 @@
  184.58    apply (reify Irint_simps ("(3::int) * x + y * y - 9 + (- z)"))
  184.59    oops
  184.60  
  184.61 -datatype_new rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
  184.62 +datatype rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
  184.63  
  184.64  primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> int list"
  184.65  where
  184.66 @@ -387,7 +387,7 @@
  184.67    apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs"))
  184.68    oops
  184.69  
  184.70 -datatype_new rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
  184.71 +datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
  184.72    | NNeg rnat | NSub rnat rnat | Nlgth rlist
  184.73  
  184.74  primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> nat list \<Rightarrow> nat"
  184.75 @@ -418,7 +418,7 @@
  184.76       ("Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs)"))
  184.77    oops
  184.78  
  184.79 -datatype_new rifm = RT | RF | RVar nat
  184.80 +datatype rifm = RT | RF | RVar nat
  184.81    | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat
  184.82    | RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm
  184.83    | RNEX rifm | RIEX rifm | RLEX rifm | RNALL rifm | RIALL rifm | RLALL rifm
  184.84 @@ -451,7 +451,7 @@
  184.85  
  184.86  text {* An example for equations containing type variables *}
  184.87  
  184.88 -datatype_new prod = Zero | One | Var nat | Mul prod prod 
  184.89 +datatype prod = Zero | One | Var nat | Mul prod prod 
  184.90    | Pw prod nat | PNM nat nat prod
  184.91  
  184.92  primrec Iprod :: " prod \<Rightarrow> ('a::linordered_idom) list \<Rightarrow>'a" 
  184.93 @@ -463,7 +463,7 @@
  184.94  | "Iprod (Pw a n) vs = Iprod a vs ^ n"
  184.95  | "Iprod (PNM n k t) vs = (vs ! n) ^ k * Iprod t vs"
  184.96  
  184.97 -datatype_new sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
  184.98 +datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
  184.99    | Or sgn sgn | And sgn sgn
 184.100  
 184.101  primrec Isgn :: "sgn \<Rightarrow> ('a::linordered_idom) list \<Rightarrow> bool"
   185.1 --- a/src/HOL/ex/Refute_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
   185.2 +++ b/src/HOL/ex/Refute_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
   185.3 @@ -605,7 +605,7 @@
   185.4  
   185.5  text {* Non-recursive datatypes *}
   185.6  
   185.7 -datatype_new T1 = A | B
   185.8 +datatype T1 = A | B
   185.9  
  185.10  lemma "P (x::T1)"
  185.11  refute [expect = genuine]
  185.12 @@ -639,7 +639,7 @@
  185.13  refute [expect = genuine]
  185.14  oops
  185.15  
  185.16 -datatype_new 'a T2 = C T1 | D 'a
  185.17 +datatype 'a T2 = C T1 | D 'a
  185.18  
  185.19  lemma "P (x::'a T2)"
  185.20  refute [expect = genuine]
  185.21 @@ -669,7 +669,7 @@
  185.22  refute [expect = genuine]
  185.23  oops
  185.24  
  185.25 -datatype_new ('a,'b) T3 = E "'a \<Rightarrow> 'b"
  185.26 +datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
  185.27  
  185.28  lemma "P (x::('a,'b) T3)"
  185.29  refute [expect = genuine]
  185.30 @@ -772,7 +772,7 @@
  185.31  refute [expect = potential]
  185.32  oops
  185.33  
  185.34 -datatype_new BitList = BitListNil | Bit0 BitList | Bit1 BitList
  185.35 +datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
  185.36  
  185.37  lemma "P (x::BitList)"
  185.38  refute [expect = potential]
   186.1 --- a/src/HOL/ex/Seq.thy	Thu Sep 11 19:26:59 2014 +0200
   186.2 +++ b/src/HOL/ex/Seq.thy	Thu Sep 11 19:32:36 2014 +0200
   186.3 @@ -8,7 +8,7 @@
   186.4  imports Main
   186.5  begin
   186.6  
   186.7 -datatype_new 'a seq = Empty | Seq 'a "'a seq"
   186.8 +datatype 'a seq = Empty | Seq 'a "'a seq"
   186.9  
  186.10  fun conc :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq"
  186.11  where
   187.1 --- a/src/HOL/ex/Serbian.thy	Thu Sep 11 19:26:59 2014 +0200
   187.2 +++ b/src/HOL/ex/Serbian.thy	Thu Sep 11 19:32:36 2014 +0200
   187.3 @@ -11,7 +11,7 @@
   187.4  begin
   187.5  
   187.6  text{* Serbian cyrillic letters *}
   187.7 -datatype_new azbuka =
   187.8 +datatype azbuka =
   187.9    azbA   ("А")
  187.10  | azbB   ("Б")
  187.11  | azbV   ("В")
  187.12 @@ -47,7 +47,7 @@
  187.13  thm azbuka.induct
  187.14  
  187.15  text{* Serbian latin letters *}
  187.16 -datatype_new abeceda =
  187.17 +datatype abeceda =
  187.18    abcA   ("A")
  187.19  | abcB   ("B")
  187.20  | abcC   ("C")
   188.1 --- a/src/HOL/ex/Sudoku.thy	Thu Sep 11 19:26:59 2014 +0200
   188.2 +++ b/src/HOL/ex/Sudoku.thy	Thu Sep 11 19:32:36 2014 +0200
   188.3 @@ -19,7 +19,7 @@
   188.4  
   188.5  no_notation Groups.one_class.one ("1")
   188.6  
   188.7 -datatype_new digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
   188.8 +datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
   188.9  
  188.10  definition valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where
  188.11  
   189.1 --- a/src/HOL/ex/Termination.thy	Thu Sep 11 19:26:59 2014 +0200
   189.2 +++ b/src/HOL/ex/Termination.thy	Thu Sep 11 19:32:36 2014 +0200
   189.3 @@ -118,7 +118,7 @@
   189.4    
   189.5  subsection {* Simple examples with other datatypes than nat, e.g. trees and lists *}
   189.6  
   189.7 -datatype_new tree = Node | Branch tree tree
   189.8 +datatype tree = Node | Branch tree tree
   189.9  
  189.10  fun g_tree :: "tree * tree \<Rightarrow> tree"
  189.11  where
   190.1 --- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Thu Sep 11 19:26:59 2014 +0200
   190.2 +++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Thu Sep 11 19:32:36 2014 +0200
   190.3 @@ -6,7 +6,7 @@
   190.4  imports "~~/src/HOL/Library/Transitive_Closure_Table"
   190.5  begin
   190.6  
   190.7 -datatype_new ty = A | B | C
   190.8 +datatype ty = A | B | C
   190.9  
  190.10  inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
  190.11  where
   191.1 --- a/src/HOL/ex/Tree23.thy	Thu Sep 11 19:26:59 2014 +0200
   191.2 +++ b/src/HOL/ex/Tree23.thy	Thu Sep 11 19:32:36 2014 +0200
   191.3 @@ -21,16 +21,16 @@
   191.4  
   191.5  type_synonym key = int -- {*for simplicity, should be a type class*}
   191.6  
   191.7 -datatype_new ord = LESS | EQUAL | GREATER
   191.8 +datatype ord = LESS | EQUAL | GREATER
   191.9  
  191.10  definition "ord i j = (if i<j then LESS else if i=j then EQUAL else GREATER)"
  191.11  
  191.12 -datatype_new 'a tree23 =
  191.13 +datatype 'a tree23 =
  191.14    Empty |
  191.15    Branch2 "'a tree23" "key * 'a" "'a tree23" |
  191.16    Branch3 "'a tree23" "key * 'a" "'a tree23" "key * 'a" "'a tree23"
  191.17  
  191.18 -datatype_new 'a growth =
  191.19 +datatype 'a growth =
  191.20    Stay "'a tree23" |
  191.21    Sprout "'a tree23" "key * 'a" "'a tree23"
  191.22  
  191.23 @@ -402,7 +402,7 @@
  191.24  text{* This is a little test harness and should be commented out once the
  191.25  above functions have been proved correct. *}
  191.26  
  191.27 -datatype_new 'a act = Add int 'a | Del int
  191.28 +datatype 'a act = Add int 'a | Del int
  191.29  
  191.30  fun exec where
  191.31  "exec [] t = t" |
   192.1 --- a/src/HOL/ex/Unification.thy	Thu Sep 11 19:26:59 2014 +0200
   192.2 +++ b/src/HOL/ex/Unification.thy	Thu Sep 11 19:32:36 2014 +0200
   192.3 @@ -32,7 +32,7 @@
   192.4  
   192.5  text {* Binary trees with leaves that are constants or variables. *}
   192.6  
   192.7 -datatype_new 'a trm = 
   192.8 +datatype 'a trm = 
   192.9    Var 'a 
  192.10    | Const 'a
  192.11    | Comb "'a trm" "'a trm" (infix "\<cdot>" 60)