use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
authorblanchet
Tue Sep 09 20:51:36 2014 +0200 (2014-09-09)
changeset 58249180f1b3508ed
parent 58248 25af24e1f37b
child 58250 bf4188deabb2
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
src/HOL/Auth/Message.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Smartcard/EventSC.thy
src/HOL/Auth/TLS.thy
src/HOL/BNF_Examples/Process.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/Codegenerator_Test/Code_Test.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/HOLCF/Discrete.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_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/Compiler.thy
src/HOL/IMP/OO.thy
src/HOL/IMP/Poly_Types.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.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
src/HOL/Imperative_HOL/ex/SatChecker.thy
src/HOL/Induct/ABexp.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/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/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/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_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/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/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
src/HOL/Statespace/DistinctTreeProver.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/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/Seq.thy
src/HOL/ex/Serbian.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/src/HOL/Auth/Message.thy	Tue Sep 09 17:51:07 2014 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Tue Sep 09 20:51:36 2014 +0200
     1.3 @@ -35,10 +35,10 @@
     1.4  definition symKeys :: "key set" where
     1.5    "symKeys == {K. invKey K = K}"
     1.6  
     1.7 -datatype  --{*We allow any number of friendly agents*}
     1.8 +datatype_new  --{*We allow any number of friendly agents*}
     1.9    agent = Server | Friend nat | Spy
    1.10  
    1.11 -datatype
    1.12 +datatype_new
    1.13       msg = Agent  agent     --{*Agent names*}
    1.14           | Number nat       --{*Ordinary integers, timestamps, ...*}
    1.15           | Nonce  nat       --{*Unguessable nonces*}
     2.1 --- a/src/HOL/Auth/Public.thy	Tue Sep 09 17:51:07 2014 +0200
     2.2 +++ b/src/HOL/Auth/Public.thy	Tue Sep 09 20:51:36 2014 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4  
     2.5  subsection{*Asymmetric Keys*}
     2.6  
     2.7 -datatype keymode = Signature | Encryption
     2.8 +datatype_new keymode = Signature | Encryption
     2.9  
    2.10  consts
    2.11    publicKey :: "[keymode,agent] => key"
     3.1 --- a/src/HOL/Auth/Smartcard/EventSC.thy	Tue Sep 09 17:51:07 2014 +0200
     3.2 +++ b/src/HOL/Auth/Smartcard/EventSC.thy	Tue Sep 09 20:51:36 2014 +0200
     3.3 @@ -9,10 +9,10 @@
     3.4  consts  (*Initial states of agents -- parameter of the construction*)
     3.5    initState :: "agent => msg set"
     3.6  
     3.7 -datatype card = Card agent
     3.8 +datatype_new card = Card agent
     3.9  
    3.10  text{*Four new events express the traffic between an agent and his card*}
    3.11 -datatype  
    3.12 +datatype_new  
    3.13    event = Says  agent agent msg
    3.14          | Notes agent       msg
    3.15          | Gets  agent       msg
     4.1 --- a/src/HOL/Auth/TLS.thy	Tue Sep 09 17:51:07 2014 +0200
     4.2 +++ b/src/HOL/Auth/TLS.thy	Tue Sep 09 20:51:36 2014 +0200
     4.3 @@ -49,7 +49,7 @@
     4.4  signature.  Therefore, we formalize signature as encryption using the
     4.5  private encryption key.*}
     4.6  
     4.7 -datatype role = ClientRole | ServerRole
     4.8 +datatype_new role = ClientRole | ServerRole
     4.9  
    4.10  consts
    4.11    (*Pseudo-random function of Section 5*)
     5.1 --- a/src/HOL/BNF_Examples/Process.thy	Tue Sep 09 17:51:07 2014 +0200
     5.2 +++ b/src/HOL/BNF_Examples/Process.thy	Tue Sep 09 20:51:36 2014 +0200
     5.3 @@ -79,7 +79,7 @@
     5.4  
     5.5  subsection{* Multi-guard fixpoint definitions, simulated with auxiliary arguments *}
     5.6  
     5.7 -datatype x_y_ax = x | y | ax
     5.8 +datatype_new x_y_ax = x | y | ax
     5.9  
    5.10  primcorec F :: "x_y_ax \<Rightarrow> char list process" where
    5.11    "xyax = x \<Longrightarrow> isChoice (F xyax)"
    5.12 @@ -106,7 +106,7 @@
    5.13  hide_const x y ax X Y AX
    5.14  
    5.15  (* Process terms *)
    5.16 -datatype ('a,'pvar) process_term =
    5.17 +datatype_new ('a,'pvar) process_term =
    5.18   VAR 'pvar |
    5.19   PROC "'a process" |
    5.20   ACT 'a "('a,'pvar) process_term" | CH "('a,'pvar) process_term" "('a,'pvar) process_term"
     6.1 --- a/src/HOL/Bali/AxSem.thy	Tue Sep 09 17:51:07 2014 +0200
     6.2 +++ b/src/HOL/Bali/AxSem.thy	Tue Sep 09 20:51:36 2014 +0200
     6.3 @@ -378,7 +378,7 @@
     6.4                               \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
     6.5                 \<and> s\<Colon>\<preceq>(G,L))"
     6.6  
     6.7 -datatype    'a triple = triple "('a assn)" "term" "('a assn)" (** should be
     6.8 +datatype_new    'a triple = triple "('a assn)" "term" "('a assn)" (** should be
     6.9  something like triple = \<forall>'a. triple ('a assn) term ('a assn)   **)
    6.10                                          ("{(1_)}/ _>/ {(1_)}"      [3,65,3]75)
    6.11  type_synonym 'a triples = "'a triple set"
     7.1 --- a/src/HOL/Bali/Basis.thy	Tue Sep 09 17:51:07 2014 +0200
     7.2 +++ b/src/HOL/Bali/Basis.thy	Tue Sep 09 20:51:36 2014 +0200
     7.3 @@ -155,7 +155,7 @@
     7.4  primrec the_Inr :: "'a + 'b \<Rightarrow> 'b"
     7.5    where "the_Inr (Inr b) = b"
     7.6  
     7.7 -datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
     7.8 +datatype_new ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
     7.9  
    7.10  primrec the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
    7.11    where "the_In1 (In1 a) = a"
     8.1 --- a/src/HOL/Bali/Decl.thy	Tue Sep 09 17:51:07 2014 +0200
     8.2 +++ b/src/HOL/Bali/Decl.thy	Tue Sep 09 20:51:36 2014 +0200
     8.3 @@ -42,7 +42,7 @@
     8.4  
     8.5  subsubsection {* Access modifier *}
     8.6  
     8.7 -datatype acc_modi (* access modifier *)
     8.8 +datatype_new acc_modi (* access modifier *)
     8.9           = Private | Package | Protected | Public 
    8.10  
    8.11  text {* 
    8.12 @@ -223,9 +223,9 @@
    8.13  introduce the notion of a member declaration (e.g. useful to define 
    8.14  accessiblity ) *}
    8.15  
    8.16 -datatype memberdecl = fdecl fdecl | mdecl mdecl
    8.17 +datatype_new memberdecl = fdecl fdecl | mdecl mdecl
    8.18  
    8.19 -datatype memberid = fid vname | mid sig
    8.20 +datatype_new memberid = fid vname | mid sig
    8.21  
    8.22  class has_memberid =
    8.23    fixes memberid :: "'a \<Rightarrow> memberid"
     9.1 --- a/src/HOL/Bali/Example.thy	Tue Sep 09 17:51:07 2014 +0200
     9.2 +++ b/src/HOL/Bali/Example.thy	Tue Sep 09 20:51:36 2014 +0200
     9.3 @@ -66,9 +66,9 @@
     9.4  section "type and expression names"
     9.5  
     9.6  (** unfortunately cannot simply instantiate tnam **)
     9.7 -datatype tnam'  = HasFoo' | Base' | Ext' | Main'
     9.8 -datatype vnam'  = arr' | vee' | z' | e'
     9.9 -datatype label' = lab1'
    9.10 +datatype_new tnam'  = HasFoo' | Base' | Ext' | Main'
    9.11 +datatype_new vnam'  = arr' | vee' | z' | e'
    9.12 +datatype_new label' = lab1'
    9.13  
    9.14  axiomatization
    9.15    tnam' :: "tnam'  \<Rightarrow> tnam" and
    10.1 --- a/src/HOL/Bali/Name.thy	Tue Sep 09 17:51:07 2014 +0200
    10.2 +++ b/src/HOL/Bali/Name.thy	Tue Sep 09 20:51:36 2014 +0200
    10.3 @@ -12,11 +12,11 @@
    10.4  typedecl vname  --{* variable or field name *}
    10.5  typedecl label  --{* label as destination of break or continue *}
    10.6  
    10.7 -datatype ename        --{* expression name *} 
    10.8 +datatype_new ename        --{* expression name *} 
    10.9          = VNam vname 
   10.10          | Res         --{* special name to model the return value of methods *}
   10.11  
   10.12 -datatype lname        --{* names for local variables and the This pointer *}
   10.13 +datatype_new lname        --{* names for local variables and the This pointer *}
   10.14          = EName ename 
   10.15          | This
   10.16  abbreviation VName   :: "vname \<Rightarrow> lname"
   10.17 @@ -25,7 +25,7 @@
   10.18  abbreviation Result :: lname
   10.19        where "Result == EName Res"
   10.20  
   10.21 -datatype xname          --{* names of standard exceptions *}
   10.22 +datatype_new xname          --{* names of standard exceptions *}
   10.23          = Throwable
   10.24          | NullPointer | OutOfMemory | ClassCast   
   10.25          | NegArrSize  | IndOutBound | ArrStore
   10.26 @@ -39,7 +39,7 @@
   10.27  done
   10.28  
   10.29  
   10.30 -datatype tname  --{* type names for standard classes and other type names *}
   10.31 +datatype_new tname  --{* type names for standard classes and other type names *}
   10.32          = Object'
   10.33          | SXcpt'   xname
   10.34          | TName   tnam
    11.1 --- a/src/HOL/Bali/State.thy	Tue Sep 09 17:51:07 2014 +0200
    11.2 +++ b/src/HOL/Bali/State.thy	Tue Sep 09 20:51:36 2014 +0200
    11.3 @@ -19,7 +19,7 @@
    11.4  
    11.5  section "objects"
    11.6  
    11.7 -datatype  obj_tag =     --{* tag for generic object   *}
    11.8 +datatype_new  obj_tag =     --{* tag for generic object   *}
    11.9            CInst qtname  --{* class instance           *}
   11.10          | Arr  ty int   --{* array with component type and length *}
   11.11      --{* | CStat qtname   the tag is irrelevant for a class object,
   11.12 @@ -225,7 +225,7 @@
   11.13   (type) "heap"   <= (type) "(loc  , obj) table"
   11.14  (*  (type) "locals" <= (type) "(lname, val) table" *)
   11.15  
   11.16 -datatype st = (* pure state, i.e. contents of all variables *)
   11.17 +datatype_new st = (* pure state, i.e. contents of all variables *)
   11.18           st globs locals
   11.19  
   11.20  subsection "access"
    12.1 --- a/src/HOL/Bali/Term.thy	Tue Sep 09 17:51:07 2014 +0200
    12.2 +++ b/src/HOL/Bali/Term.thy	Tue Sep 09 20:51:36 2014 +0200
    12.3 @@ -60,20 +60,20 @@
    12.4  type_synonym locals = "(lname, val) table"  --{* local variables *}
    12.5  
    12.6  
    12.7 -datatype jump
    12.8 +datatype_new jump
    12.9          = Break label --{* break *}
   12.10          | Cont label  --{* continue *}
   12.11          | Ret         --{* return from method *}
   12.12  
   12.13 -datatype xcpt        --{* exception *}
   12.14 +datatype_new xcpt        --{* exception *}
   12.15          = Loc loc    --{* location of allocated execption object *}
   12.16          | Std xname  --{* intermediate standard exception, see Eval.thy *}
   12.17  
   12.18 -datatype error
   12.19 +datatype_new error
   12.20         =  AccessViolation  --{* Access to a member that isn't permitted *}
   12.21          | CrossMethodJump  --{* Method exits with a break or continue *}
   12.22  
   12.23 -datatype abrupt       --{* abrupt completion *} 
   12.24 +datatype_new abrupt       --{* abrupt completion *} 
   12.25          = Xcpt xcpt   --{* exception *}
   12.26          | Jump jump   --{* break, continue, return *}
   12.27          | Error error -- {* runtime errors, we wan't to detect and proof absent
   12.28 @@ -90,7 +90,7 @@
   12.29  translations
   12.30   (type) "locals" <= (type) "(lname, val) table"
   12.31  
   12.32 -datatype inv_mode                  --{* invocation mode for method calls *}
   12.33 +datatype_new inv_mode                  --{* invocation mode for method calls *}
   12.34          = Static                   --{* static *}
   12.35          | SuperM                   --{* super  *}
   12.36          | IntVir                   --{* interface or virtual *}
   12.37 @@ -104,13 +104,13 @@
   12.38    (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
   12.39  
   12.40  --{* function codes for unary operations *}
   12.41 -datatype unop =  UPlus    -- {*{\tt +} unary plus*} 
   12.42 +datatype_new unop =  UPlus    -- {*{\tt +} unary plus*} 
   12.43                 | UMinus   -- {*{\tt -} unary minus*}
   12.44                 | UBitNot  -- {*{\tt ~} bitwise NOT*}
   12.45                 | UNot     -- {*{\tt !} logical complement*}
   12.46  
   12.47  --{* function codes for binary operations *}
   12.48 -datatype binop = Mul     -- {*{\tt * }   multiplication*}
   12.49 +datatype_new binop = Mul     -- {*{\tt * }   multiplication*}
   12.50                 | Div     -- {*{\tt /}   division*}
   12.51                 | Mod     -- {*{\tt \%}   remainder*}
   12.52                 | Plus    -- {*{\tt +}   addition*}
   12.53 @@ -140,7 +140,7 @@
   12.54        {\tt true || e} e is not evaluated; 
   12.55  *}
   12.56  
   12.57 -datatype var
   12.58 +datatype_new var
   12.59          = LVar lname --{* local variable (incl. parameters) *}
   12.60          | FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90)
   12.61                       --{* class field *}
    13.1 --- a/src/HOL/Bali/Type.thy	Tue Sep 09 17:51:07 2014 +0200
    13.2 +++ b/src/HOL/Bali/Type.thy	Tue Sep 09 20:51:36 2014 +0200
    13.3 @@ -14,13 +14,13 @@
    13.4  \end{itemize}
    13.5  *}
    13.6  
    13.7 -datatype prim_ty        --{* primitive type, cf. 4.2 *}
    13.8 +datatype_new prim_ty        --{* primitive type, cf. 4.2 *}
    13.9          = Void          --{* result type of void methods *}
   13.10          | Boolean
   13.11          | Integer
   13.12  
   13.13  
   13.14 -datatype ref_ty         --{* reference type, cf. 4.3 *}
   13.15 +datatype_new ref_ty         --{* reference type, cf. 4.3 *}
   13.16          = NullT         --{* null type, cf. 4.1 *}
   13.17          | IfaceT qtname --{* interface type *}
   13.18          | ClassT qtname --{* class type *}
    14.1 --- a/src/HOL/Bali/Value.thy	Tue Sep 09 17:51:07 2014 +0200
    14.2 +++ b/src/HOL/Bali/Value.thy	Tue Sep 09 20:51:36 2014 +0200
    14.3 @@ -9,7 +9,7 @@
    14.4  
    14.5  typedecl loc            --{* locations, i.e. abstract references on objects *}
    14.6  
    14.7 -datatype val
    14.8 +datatype_new val
    14.9          = Unit          --{* dummy result value of void methods *}
   14.10          | Bool bool     --{* Boolean value *}
   14.11          | Intg int      --{* integer value *}
    15.1 --- a/src/HOL/Codegenerator_Test/Code_Test.thy	Tue Sep 09 17:51:07 2014 +0200
    15.2 +++ b/src/HOL/Codegenerator_Test/Code_Test.thy	Tue Sep 09 20:51:36 2014 +0200
    15.3 @@ -11,7 +11,7 @@
    15.4  
    15.5  subsection {* YXML encoding for @{typ Code_Evaluation.term} *}
    15.6  
    15.7 -datatype yxml_of_term = YXML
    15.8 +datatype_new yxml_of_term = YXML
    15.9  
   15.10  lemma yot_anything: "x = (y :: yxml_of_term)"
   15.11  by(cases x y rule: yxml_of_term.exhaust[case_product yxml_of_term.exhaust])(simp)
   15.12 @@ -58,7 +58,7 @@
   15.13    sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}.
   15.14  *}
   15.15  
   15.16 -datatype xml_tree = XML_Tree
   15.17 +datatype_new xml_tree = XML_Tree
   15.18  
   15.19  lemma xml_tree_anything: "x = (y :: xml_tree)"
   15.20  by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)
    16.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Sep 09 17:51:07 2014 +0200
    16.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Sep 09 20:51:36 2014 +0200
    16.3 @@ -2037,7 +2037,7 @@
    16.4  
    16.5  subsection "Define syntax and semantics"
    16.6  
    16.7 -datatype floatarith
    16.8 +datatype_new floatarith
    16.9    = Add floatarith floatarith
   16.10    | Minus floatarith
   16.11    | Mult floatarith floatarith
   16.12 @@ -2456,7 +2456,7 @@
   16.13    show ?case by (cases "n < length vs", auto)
   16.14  qed
   16.15  
   16.16 -datatype form = Bound floatarith floatarith floatarith form
   16.17 +datatype_new form = Bound floatarith floatarith floatarith form
   16.18                | Assign floatarith floatarith form
   16.19                | Less floatarith floatarith
   16.20                | LessEqual floatarith floatarith
    17.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue Sep 09 17:51:07 2014 +0200
    17.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue Sep 09 20:51:36 2014 +0200
    17.3 @@ -11,12 +11,12 @@
    17.4  
    17.5  text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
    17.6  
    17.7 -datatype 'a pol =
    17.8 +datatype_new 'a pol =
    17.9      Pc 'a
   17.10    | Pinj nat "'a pol"
   17.11    | PX "'a pol" nat "'a pol"
   17.12  
   17.13 -datatype 'a polex =
   17.14 +datatype_new 'a polex =
   17.15      Pol "'a pol"
   17.16    | Add "'a polex" "'a polex"
   17.17    | Sub "'a polex" "'a polex"
    18.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Tue Sep 09 17:51:07 2014 +0200
    18.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Tue Sep 09 20:51:36 2014 +0200
    18.3 @@ -15,7 +15,7 @@
    18.4  (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    18.5  (*********************************************************************************)
    18.6  
    18.7 -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
    18.8 +datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
    18.9    | Mul int num
   18.10  
   18.11  primrec num_size :: "num \<Rightarrow> nat" -- {* A size for num to make inductive proofs simpler *}
   18.12 @@ -38,7 +38,7 @@
   18.13  | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
   18.14  | "Inum bs (Mul c a) = c* Inum bs a"
   18.15  
   18.16 -datatype fm  =
   18.17 +datatype_new fm  =
   18.18    T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
   18.19    NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
   18.20    | Closed nat | NClosed nat
    19.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Tue Sep 09 17:51:07 2014 +0200
    19.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Tue Sep 09 20:51:36 2014 +0200
    19.3 @@ -13,7 +13,7 @@
    19.4    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    19.5    (*********************************************************************************)
    19.6  
    19.7 -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 
    19.8 +datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 
    19.9    | Mul int num 
   19.10  
   19.11    (* A size for num to make inductive proofs simpler*)
   19.12 @@ -36,7 +36,7 @@
   19.13  | "Inum bs (Sub a b) = Inum bs a - Inum bs b"
   19.14  | "Inum bs (Mul c a) = (real c) * Inum bs a"
   19.15      (* FORMULAE *)
   19.16 -datatype fm  = 
   19.17 +datatype_new fm  = 
   19.18    T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num|
   19.19    NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
   19.20  
    20.1 --- a/src/HOL/Decision_Procs/MIR.thy	Tue Sep 09 17:51:07 2014 +0200
    20.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Tue Sep 09 20:51:36 2014 +0200
    20.3 @@ -105,7 +105,7 @@
    20.4    (****                            SHADOW SYNTAX AND SEMANTICS                  ****)
    20.5    (*********************************************************************************)
    20.6  
    20.7 -datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 
    20.8 +datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num 
    20.9    | Mul int num | Floor num| CF int num num
   20.10  
   20.11    (* A size for num to make inductive proofs simpler*)
   20.12 @@ -188,7 +188,7 @@
   20.13  
   20.14  
   20.15      (* FORMULAE *)
   20.16 -datatype fm  = 
   20.17 +datatype_new fm  = 
   20.18    T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
   20.19    NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
   20.20  
    21.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Sep 09 17:51:07 2014 +0200
    21.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Sep 09 20:51:36 2014 +0200
    21.3 @@ -15,7 +15,7 @@
    21.4  
    21.5  subsection {* Terms *}
    21.6  
    21.7 -datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm
    21.8 +datatype_new tm = CP poly | Bound nat | Add tm tm | Mul poly tm
    21.9    | Neg tm | Sub tm tm | CNP nat poly tm
   21.10  
   21.11  (* A size for poly to make inductive proofs simpler*)
   21.12 @@ -493,7 +493,7 @@
   21.13  
   21.14  subsection{* Formulae *}
   21.15  
   21.16 -datatype fm  =  T| F| Le tm | Lt tm | Eq tm | NEq tm|
   21.17 +datatype_new fm  =  T| F| Le tm | Lt tm | Eq tm | NEq tm|
   21.18    NOT fm| And fm fm|  Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
   21.19  
   21.20  
    22.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Sep 09 17:51:07 2014 +0200
    22.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Sep 09 20:51:36 2014 +0200
    22.3 @@ -10,7 +10,7 @@
    22.4  
    22.5  subsection{* Datatype of polynomial expressions *}
    22.6  
    22.7 -datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly
    22.8 +datatype_new poly = C Num | Bound nat | Add poly poly | Sub poly poly
    22.9    | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
   22.10  
   22.11  abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
    23.1 --- a/src/HOL/HOLCF/Discrete.thy	Tue Sep 09 17:51:07 2014 +0200
    23.2 +++ b/src/HOL/HOLCF/Discrete.thy	Tue Sep 09 20:51:36 2014 +0200
    23.3 @@ -8,7 +8,7 @@
    23.4  imports Cont
    23.5  begin
    23.6  
    23.7 -datatype 'a discr = Discr "'a :: type"
    23.8 +datatype_new 'a discr = Discr "'a :: type"
    23.9  
   23.10  subsection {* Discrete cpo class instance *}
   23.11  
    24.1 --- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Tue Sep 09 17:51:07 2014 +0200
    24.2 +++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Tue Sep 09 20:51:36 2014 +0200
    24.3 @@ -8,7 +8,7 @@
    24.4  imports IOA Action Lemmas
    24.5  begin
    24.6  
    24.7 -datatype 'a abs_action = S 'a | R 'a
    24.8 +datatype_new 'a abs_action = S 'a | R 'a
    24.9  
   24.10  
   24.11  (**********************************************************
    25.1 --- a/src/HOL/HOLCF/IOA/ABP/Action.thy	Tue Sep 09 17:51:07 2014 +0200
    25.2 +++ b/src/HOL/HOLCF/IOA/ABP/Action.thy	Tue Sep 09 20:51:36 2014 +0200
    25.3 @@ -8,7 +8,7 @@
    25.4  imports Packet
    25.5  begin
    25.6  
    25.7 -datatype 'm action =
    25.8 +datatype_new 'm action =
    25.9      Next | S_msg 'm | R_msg 'm
   25.10    | S_pkt "'m packet" | R_pkt "'m packet"
   25.11    | S_ack bool | R_ack bool
    26.1 --- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Tue Sep 09 17:51:07 2014 +0200
    26.2 +++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Tue Sep 09 20:51:36 2014 +0200
    26.3 @@ -8,7 +8,7 @@
    26.4  imports IOA Action
    26.5  begin
    26.6  
    26.7 -datatype 'a abs_action = S 'a | R 'a
    26.8 +datatype_new 'a abs_action = S 'a | R 'a
    26.9  
   26.10  definition
   26.11    ch_asig :: "'a abs_action signature" where
    27.1 --- a/src/HOL/HOLCF/IOA/NTP/Action.thy	Tue Sep 09 17:51:07 2014 +0200
    27.2 +++ b/src/HOL/HOLCF/IOA/NTP/Action.thy	Tue Sep 09 20:51:36 2014 +0200
    27.3 @@ -8,7 +8,7 @@
    27.4  imports Packet
    27.5  begin
    27.6  
    27.7 -datatype 'm action = S_msg 'm | R_msg 'm
    27.8 +datatype_new 'm action = S_msg 'm | R_msg 'm
    27.9                     | S_pkt "'m packet" | R_pkt "'m packet"
   27.10                     | S_ack bool | R_ack bool
   27.11                     | C_m_s | C_m_r | C_r_s | C_r_r 'm
    28.1 --- a/src/HOL/HOLCF/IOA/Storage/Action.thy	Tue Sep 09 17:51:07 2014 +0200
    28.2 +++ b/src/HOL/HOLCF/IOA/Storage/Action.thy	Tue Sep 09 20:51:36 2014 +0200
    28.3 @@ -8,7 +8,7 @@
    28.4  imports Main
    28.5  begin
    28.6  
    28.7 -datatype action = New | Loc nat | Free nat
    28.8 +datatype_new action = New | Loc nat | Free nat
    28.9  
   28.10  lemma [cong]: "!!x. x = y ==> case_action a b c x = case_action a b c y"
   28.11    by simp
    29.1 --- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Tue Sep 09 17:51:07 2014 +0200
    29.2 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Tue Sep 09 20:51:36 2014 +0200
    29.3 @@ -8,7 +8,7 @@
    29.4  imports Abstraction
    29.5  begin
    29.6  
    29.7 -datatype action = INC
    29.8 +datatype_new action = INC
    29.9  
   29.10  definition
   29.11    C_asig :: "action signature" where
    30.1 --- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Tue Sep 09 17:51:07 2014 +0200
    30.2 +++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Tue Sep 09 20:51:36 2014 +0200
    30.3 @@ -8,7 +8,7 @@
    30.4  imports IOA Abstraction
    30.5  begin
    30.6  
    30.7 -datatype action = INC
    30.8 +datatype_new action = INC
    30.9  
   30.10  definition
   30.11    C_asig :: "action signature" where
    31.1 --- a/src/HOL/HOLCF/Up.thy	Tue Sep 09 17:51:07 2014 +0200
    31.2 +++ b/src/HOL/HOLCF/Up.thy	Tue Sep 09 20:51:36 2014 +0200
    31.3 @@ -13,7 +13,7 @@
    31.4  
    31.5  subsection {* Definition of new type for lifting *}
    31.6  
    31.7 -datatype 'a u = Ibottom | Iup 'a
    31.8 +datatype_new 'a u = Ibottom | Iup 'a
    31.9  
   31.10  type_notation (xsymbols)
   31.11    u  ("(_\<^sub>\<bottom>)" [1000] 999)
    32.1 --- a/src/HOL/Hoare/Heap.thy	Tue Sep 09 17:51:07 2014 +0200
    32.2 +++ b/src/HOL/Hoare/Heap.thy	Tue Sep 09 20:51:36 2014 +0200
    32.3 @@ -10,7 +10,7 @@
    32.4  
    32.5  subsection "References"
    32.6  
    32.7 -datatype 'a ref = Null | Ref 'a
    32.8 +datatype_new 'a ref = Null | Ref 'a
    32.9  
   32.10  lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
   32.11    by (induct x) auto
    33.1 --- a/src/HOL/Hoare_Parallel/Graph.thy	Tue Sep 09 17:51:07 2014 +0200
    33.2 +++ b/src/HOL/Hoare_Parallel/Graph.thy	Tue Sep 09 20:51:36 2014 +0200
    33.3 @@ -4,7 +4,7 @@
    33.4  
    33.5  theory Graph imports Main begin
    33.6  
    33.7 -datatype node = Black | White
    33.8 +datatype_new node = Black | White
    33.9  
   33.10  type_synonym nodes = "node list"
   33.11  type_synonym edge = "nat \<times> nat"
    34.1 --- a/src/HOL/Hoare_Parallel/OG_Com.thy	Tue Sep 09 17:51:07 2014 +0200
    34.2 +++ b/src/HOL/Hoare_Parallel/OG_Com.thy	Tue Sep 09 20:51:36 2014 +0200
    34.3 @@ -14,7 +14,7 @@
    34.4  datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a
    34.5  com"} for non-annotated commands. *}
    34.6  
    34.7 -datatype 'a ann_com = 
    34.8 +datatype_new 'a ann_com = 
    34.9       AnnBasic "('a assn)"  "('a \<Rightarrow> 'a)"         
   34.10     | AnnSeq "('a ann_com)"  "('a ann_com)"   
   34.11     | AnnCond1 "('a assn)"  "('a bexp)"  "('a ann_com)"  "('a ann_com)" 
    35.1 --- a/src/HOL/Hoare_Parallel/RG_Com.thy	Tue Sep 09 17:51:07 2014 +0200
    35.2 +++ b/src/HOL/Hoare_Parallel/RG_Com.thy	Tue Sep 09 20:51:36 2014 +0200
    35.3 @@ -12,7 +12,7 @@
    35.4  
    35.5  type_synonym 'a bexp = "'a set"
    35.6  
    35.7 -datatype 'a com = 
    35.8 +datatype_new 'a com = 
    35.9      Basic "'a \<Rightarrow>'a"
   35.10    | Seq "'a com" "'a com"
   35.11    | Cond "'a bexp" "'a com" "'a com"         
    36.1 --- a/src/HOL/IMP/ACom.thy	Tue Sep 09 17:51:07 2014 +0200
    36.2 +++ b/src/HOL/IMP/ACom.thy	Tue Sep 09 20:51:36 2014 +0200
    36.3 @@ -6,7 +6,7 @@
    36.4  
    36.5  subsection "Annotated Commands"
    36.6  
    36.7 -datatype 'a acom =
    36.8 +datatype_new 'a acom =
    36.9    SKIP 'a                           ("SKIP {_}" 61) |
   36.10    Assign vname aexp 'a              ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
   36.11    Seq "('a acom)" "('a acom)"       ("_;;//_"  [60, 61] 60) |
    37.1 --- a/src/HOL/IMP/AExp.thy	Tue Sep 09 17:51:07 2014 +0200
    37.2 +++ b/src/HOL/IMP/AExp.thy	Tue Sep 09 20:51:36 2014 +0200
    37.3 @@ -9,7 +9,7 @@
    37.4  type_synonym state = "vname \<Rightarrow> val"
    37.5  
    37.6  text_raw{*\snip{AExpaexpdef}{2}{1}{% *}
    37.7 -datatype aexp = N int | V vname | Plus aexp aexp
    37.8 +datatype_new aexp = N int | V vname | Plus aexp aexp
    37.9  text_raw{*}%endsnip*}
   37.10  
   37.11  text_raw{*\snip{AExpavaldef}{1}{2}{% *}
    38.1 --- a/src/HOL/IMP/ASM.thy	Tue Sep 09 17:51:07 2014 +0200
    38.2 +++ b/src/HOL/IMP/ASM.thy	Tue Sep 09 20:51:36 2014 +0200
    38.3 @@ -5,7 +5,7 @@
    38.4  subsection "Stack Machine"
    38.5  
    38.6  text_raw{*\snip{ASMinstrdef}{0}{1}{% *}
    38.7 -datatype instr = LOADI val | LOAD vname | ADD
    38.8 +datatype_new instr = LOADI val | LOAD vname | ADD
    38.9  text_raw{*}%endsnip*}
   38.10  
   38.11  text_raw{*\snip{ASMstackdef}{1}{2}{% *}
    39.1 --- a/src/HOL/IMP/Abs_Int1_const.thy	Tue Sep 09 17:51:07 2014 +0200
    39.2 +++ b/src/HOL/IMP/Abs_Int1_const.thy	Tue Sep 09 20:51:36 2014 +0200
    39.3 @@ -6,7 +6,7 @@
    39.4  
    39.5  subsection "Constant Propagation"
    39.6  
    39.7 -datatype const = Const val | Any
    39.8 +datatype_new const = Const val | Any
    39.9  
   39.10  fun \<gamma>_const where
   39.11  "\<gamma>_const (Const i) = {i}" |
    40.1 --- a/src/HOL/IMP/Abs_Int1_parity.thy	Tue Sep 09 17:51:07 2014 +0200
    40.2 +++ b/src/HOL/IMP/Abs_Int1_parity.thy	Tue Sep 09 20:51:36 2014 +0200
    40.3 @@ -6,7 +6,7 @@
    40.4  
    40.5  subsection "Parity Analysis"
    40.6  
    40.7 -datatype parity = Even | Odd | Either
    40.8 +datatype_new parity = Even | Odd | Either
    40.9  
   40.10  text{* Instantiation of class @{class order} with type @{typ parity}: *}
   40.11  
    41.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Tue Sep 09 17:51:07 2014 +0200
    41.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Tue Sep 09 20:51:36 2014 +0200
    41.3 @@ -6,7 +6,7 @@
    41.4  
    41.5  subsection "Constant Propagation"
    41.6  
    41.7 -datatype cval = Const val | Any
    41.8 +datatype_new cval = Const val | Any
    41.9  
   41.10  fun rep_cval where
   41.11  "rep_cval (Const n) = {n}" |
    42.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Tue Sep 09 17:51:07 2014 +0200
    42.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Tue Sep 09 20:51:36 2014 +0200
    42.3 @@ -6,7 +6,7 @@
    42.4  
    42.5  subsection "Interval Analysis"
    42.6  
    42.7 -datatype ivl = I "int option" "int option"
    42.8 +datatype_new ivl = I "int option" "int option"
    42.9  
   42.10  text{* We assume an important invariant: arithmetic operations are never
   42.11  applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j <
    43.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy	Tue Sep 09 17:51:07 2014 +0200
    43.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy	Tue Sep 09 20:51:36 2014 +0200
    43.3 @@ -10,7 +10,7 @@
    43.4  
    43.5  text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
    43.6  
    43.7 -datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
    43.8 +datatype_new 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
    43.9  
   43.10  fun "fun" where "fun (FunDom f _) = f"
   43.11  fun dom where "dom (FunDom _ A) = A"
    44.1 --- a/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy	Tue Sep 09 17:51:07 2014 +0200
    44.2 +++ b/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy	Tue Sep 09 20:51:36 2014 +0200
    44.3 @@ -6,7 +6,7 @@
    44.4  
    44.5  subsection "Annotated Commands"
    44.6  
    44.7 -datatype 'a acom =
    44.8 +datatype_new 'a acom =
    44.9    SKIP 'a                           ("SKIP {_}" 61) |
   44.10    Assign vname aexp 'a              ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
   44.11    Seq "('a acom)" "('a acom)"       ("_;;//_"  [60, 61] 60) |
    45.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Tue Sep 09 17:51:07 2014 +0200
    45.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Tue Sep 09 20:51:36 2014 +0200
    45.3 @@ -6,7 +6,7 @@
    45.4  
    45.5  subsection "Constant Propagation"
    45.6  
    45.7 -datatype const = Const val | Any
    45.8 +datatype_new const = Const val | Any
    45.9  
   45.10  fun \<gamma>_const where
   45.11  "\<gamma>_const (Const n) = {n}" |
    46.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Tue Sep 09 17:51:07 2014 +0200
    46.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Tue Sep 09 20:51:36 2014 +0200
    46.3 @@ -6,7 +6,7 @@
    46.4  
    46.5  subsection "Parity Analysis"
    46.6  
    46.7 -datatype parity = Even | Odd | Either
    46.8 +datatype_new parity = Even | Odd | Either
    46.9  
   46.10  text{* Instantiation of class @{class preord} with type @{typ parity}: *}
   46.11  
    47.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy	Tue Sep 09 17:51:07 2014 +0200
    47.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy	Tue Sep 09 20:51:36 2014 +0200
    47.3 @@ -6,7 +6,7 @@
    47.4  
    47.5  subsection "Interval Analysis"
    47.6  
    47.7 -datatype ivl = I "int option" "int option"
    47.8 +datatype_new ivl = I "int option" "int option"
    47.9  
   47.10  definition "\<gamma>_ivl i = (case i of
   47.11    I (Some l) (Some h) \<Rightarrow> {l..h} |
    48.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy	Tue Sep 09 17:51:07 2014 +0200
    48.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy	Tue Sep 09 20:51:36 2014 +0200
    48.3 @@ -10,7 +10,7 @@
    48.4  
    48.5  text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
    48.6  
    48.7 -datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
    48.8 +datatype_new 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
    48.9  
   48.10  fun "fun" where "fun (FunDom f xs) = f"
   48.11  fun dom where "dom (FunDom f xs) = xs"
    49.1 --- a/src/HOL/IMP/BExp.thy	Tue Sep 09 17:51:07 2014 +0200
    49.2 +++ b/src/HOL/IMP/BExp.thy	Tue Sep 09 20:51:36 2014 +0200
    49.3 @@ -2,7 +2,7 @@
    49.4  
    49.5  subsection "Boolean Expressions"
    49.6  
    49.7 -datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
    49.8 +datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
    49.9  
   49.10  text_raw{*\snip{BExpbvaldef}{1}{2}{% *}
   49.11  fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
    50.1 --- a/src/HOL/IMP/C_like.thy	Tue Sep 09 17:51:07 2014 +0200
    50.2 +++ b/src/HOL/IMP/C_like.thy	Tue Sep 09 20:51:36 2014 +0200
    50.3 @@ -4,14 +4,14 @@
    50.4  
    50.5  type_synonym state = "nat \<Rightarrow> nat"
    50.6  
    50.7 -datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp
    50.8 +datatype_new aexp = N nat | Deref aexp ("!") | Plus aexp aexp
    50.9  
   50.10  fun aval :: "aexp \<Rightarrow> state \<Rightarrow> nat" where
   50.11  "aval (N n) s = n" |
   50.12  "aval (!a) s = s(aval a s)" |
   50.13  "aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"
   50.14  
   50.15 -datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
   50.16 +datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
   50.17  
   50.18  primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
   50.19  "bval (Bc v) _ = v" |
   50.20 @@ -20,7 +20,7 @@
   50.21  "bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"
   50.22  
   50.23  
   50.24 -datatype
   50.25 +datatype_new
   50.26    com = SKIP 
   50.27        | Assign aexp aexp         ("_ ::= _" [61, 61] 61)
   50.28        | New    aexp aexp
    51.1 --- a/src/HOL/IMP/Compiler.thy	Tue Sep 09 17:51:07 2014 +0200
    51.2 +++ b/src/HOL/IMP/Compiler.thy	Tue Sep 09 20:51:36 2014 +0200
    51.3 @@ -43,7 +43,7 @@
    51.4  subsection "Instructions and Stack Machine"
    51.5  
    51.6  text_raw{*\snip{instrdef}{0}{1}{% *}
    51.7 -datatype instr = 
    51.8 +datatype_new instr = 
    51.9    LOADI int | LOAD vname | ADD | STORE vname |
   51.10    JMP int | JMPLESS int | JMPGE int
   51.11  text_raw{*}%endsnip*}
    52.1 --- a/src/HOL/IMP/OO.thy	Tue Sep 09 17:51:07 2014 +0200
    52.2 +++ b/src/HOL/IMP/OO.thy	Tue Sep 09 20:51:36 2014 +0200
    52.3 @@ -8,13 +8,13 @@
    52.4  where "f(x,y := z) == f(x := (f x)(y := z))"
    52.5  
    52.6  type_synonym addr = nat
    52.7 -datatype ref = null | Ref addr
    52.8 +datatype_new ref = null | Ref addr
    52.9  
   52.10  type_synonym obj = "string \<Rightarrow> ref"
   52.11  type_synonym venv = "string \<Rightarrow> ref"
   52.12  type_synonym store = "addr \<Rightarrow> obj"
   52.13  
   52.14 -datatype exp =
   52.15 +datatype_new exp =
   52.16    Null |
   52.17    New |
   52.18    V string |
    53.1 --- a/src/HOL/IMP/Poly_Types.thy	Tue Sep 09 17:51:07 2014 +0200
    53.2 +++ b/src/HOL/IMP/Poly_Types.thy	Tue Sep 09 20:51:36 2014 +0200
    53.3 @@ -2,7 +2,7 @@
    53.4  
    53.5  subsection "Type Variables"
    53.6  
    53.7 -datatype ty = Ity | Rty | TV nat
    53.8 +datatype_new ty = Ity | Rty | TV nat
    53.9  
   53.10  text{* Everything else remains the same. *}
   53.11  
    54.1 --- a/src/HOL/IMP/Types.thy	Tue Sep 09 17:51:07 2014 +0200
    54.2 +++ b/src/HOL/IMP/Types.thy	Tue Sep 09 20:51:36 2014 +0200
    54.3 @@ -7,13 +7,13 @@
    54.4  
    54.5  subsection "Arithmetic Expressions"
    54.6  
    54.7 -datatype val = Iv int | Rv real
    54.8 +datatype_new val = Iv int | Rv real
    54.9  
   54.10  type_synonym vname = string
   54.11  type_synonym state = "vname \<Rightarrow> val"
   54.12  
   54.13  text_raw{*\snip{aexptDef}{0}{2}{% *}
   54.14 -datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp
   54.15 +datatype_new aexp =  Ic int | Rc real | V vname | Plus aexp aexp
   54.16  text_raw{*}%endsnip*}
   54.17  
   54.18  inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
   54.19 @@ -32,7 +32,7 @@
   54.20  
   54.21  subsection "Boolean Expressions"
   54.22  
   54.23 -datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
   54.24 +datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
   54.25  
   54.26  inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
   54.27  "tbval (Bc v) s v" |
   54.28 @@ -44,7 +44,7 @@
   54.29  subsection "Syntax of Commands"
   54.30  (* a copy of Com.thy - keep in sync! *)
   54.31  
   54.32 -datatype
   54.33 +datatype_new
   54.34    com = SKIP 
   54.35        | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
   54.36        | Seq    com  com         ("_;; _"  [60, 61] 60)
   54.37 @@ -71,7 +71,7 @@
   54.38  
   54.39  subsection "The Type System"
   54.40  
   54.41 -datatype ty = Ity | Rty
   54.42 +datatype_new ty = Ity | Rty
   54.43  
   54.44  type_synonym tyenv = "vname \<Rightarrow> ty"
   54.45  
    55.1 --- a/src/HOL/IMP/VCG.thy	Tue Sep 09 17:51:07 2014 +0200
    55.2 +++ b/src/HOL/IMP/VCG.thy	Tue Sep 09 20:51:36 2014 +0200
    55.3 @@ -7,7 +7,7 @@
    55.4  text{* Annotated commands: commands where loops are annotated with
    55.5  invariants. *}
    55.6  
    55.7 -datatype acom =
    55.8 +datatype_new acom =
    55.9    Askip                  ("SKIP") |
   55.10    Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
   55.11    Aseq   acom acom       ("_;;/ _"  [60, 61] 60) |
    56.1 --- a/src/HOL/IMPP/Com.thy	Tue Sep 09 17:51:07 2014 +0200
    56.2 +++ b/src/HOL/IMPP/Com.thy	Tue Sep 09 20:51:36 2014 +0200
    56.3 @@ -18,10 +18,10 @@
    56.4    Arg :: loc and
    56.5    Res :: loc
    56.6  
    56.7 -datatype vname  = Glb glb | Loc loc
    56.8 +datatype_new vname  = Glb glb | Loc loc
    56.9  type_synonym globs = "glb => val"
   56.10  type_synonym locals = "loc => val"
   56.11 -datatype state  = st globs locals
   56.12 +datatype_new state  = st globs locals
   56.13  (* for the meta theory, the following would be sufficient:
   56.14  typedecl state
   56.15  consts   st :: "[globs , locals] => state"
   56.16 @@ -31,7 +31,7 @@
   56.17  
   56.18  typedecl pname
   56.19  
   56.20 -datatype com
   56.21 +datatype_new com
   56.22        = SKIP
   56.23        | Ass   vname aexp        ("_:==_"                [65, 65    ] 60)
   56.24        | Local loc aexp com      ("LOCAL _:=_ IN _"      [65,  0, 61] 60)
    57.1 --- a/src/HOL/IMPP/Hoare.thy	Tue Sep 09 17:51:07 2014 +0200
    57.2 +++ b/src/HOL/IMPP/Hoare.thy	Tue Sep 09 20:51:36 2014 +0200
    57.3 @@ -28,7 +28,7 @@
    57.4    peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35) where
    57.5    "peek_and P p = (%Z s. P Z s & p s)"
    57.6  
    57.7 -datatype 'a triple =
    57.8 +datatype_new 'a triple =
    57.9    triple "'a assn"  com  "'a assn"       ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58)
   57.10  
   57.11  definition
    58.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Tue Sep 09 17:51:07 2014 +0200
    58.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Tue Sep 09 20:51:36 2014 +0200
    58.3 @@ -53,8 +53,8 @@
    58.4  definition empty :: heap where
    58.5    "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>"
    58.6  
    58.7 -datatype 'a array = Array addr
    58.8 -datatype 'a ref = Ref addr -- "note the phantom type 'a "
    58.9 +datatype_new 'a array = Array addr
   58.10 +datatype_new 'a ref = Ref addr -- "note the phantom type 'a "
   58.11  
   58.12  primrec addr_of_array :: "'a array \<Rightarrow> addr" where
   58.13    "addr_of_array (Array x) = x"
    59.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Sep 09 17:51:07 2014 +0200
    59.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Sep 09 20:51:36 2014 +0200
    59.3 @@ -16,7 +16,7 @@
    59.4  
    59.5  text {* Monadic heap actions either produce values
    59.6    and transform the heap, or fail *}
    59.7 -datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
    59.8 +datatype_new 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
    59.9  
   59.10  lemma [code, code del]:
   59.11    "(Code_Evaluation.term_of :: 'a::typerep Heap \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of"
    60.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Sep 09 17:51:07 2014 +0200
    60.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Sep 09 20:51:36 2014 +0200
    60.3 @@ -11,7 +11,7 @@
    60.4  section {* Definition of Linked Lists *}
    60.5  
    60.6  setup {* Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>type ref"}) *}
    60.7 -datatype 'a node = Empty | Node 'a "('a node) ref"
    60.8 +datatype_new 'a node = Empty | Node 'a "('a node) ref"
    60.9  
   60.10  primrec
   60.11    node_encode :: "'a\<Colon>countable node \<Rightarrow> nat"
    61.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Sep 09 17:51:07 2014 +0200
    61.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Sep 09 20:51:36 2014 +0200
    61.3 @@ -20,7 +20,7 @@
    61.4  text {* This resembles exactly to Isat's Proof Steps *}
    61.5  
    61.6  type_synonym Resolvants = "ClauseId * (Lit * ClauseId) list"
    61.7 -datatype ProofStep =
    61.8 +datatype_new ProofStep =
    61.9    ProofDone bool
   61.10    | Root ClauseId Clause
   61.11    | Conflict ClauseId Resolvants
    62.1 --- a/src/HOL/Induct/ABexp.thy	Tue Sep 09 17:51:07 2014 +0200
    62.2 +++ b/src/HOL/Induct/ABexp.thy	Tue Sep 09 20:51:36 2014 +0200
    62.3 @@ -8,7 +8,7 @@
    62.4  imports Main
    62.5  begin
    62.6  
    62.7 -datatype 'a aexp =
    62.8 +datatype_new 'a aexp =
    62.9      IF "'a bexp"  "'a aexp"  "'a aexp"
   62.10    | Sum "'a aexp"  "'a aexp"
   62.11    | Diff "'a aexp"  "'a aexp"
    63.1 --- a/src/HOL/Induct/Comb.thy	Tue Sep 09 17:51:07 2014 +0200
    63.2 +++ b/src/HOL/Induct/Comb.thy	Tue Sep 09 20:51:36 2014 +0200
    63.3 @@ -20,7 +20,7 @@
    63.4  
    63.5  text {* Datatype definition of combinators @{text S} and @{text K}. *}
    63.6  
    63.7 -datatype comb = K
    63.8 +datatype_new comb = K
    63.9                | S
   63.10                | Ap comb comb (infixl "##" 90)
   63.11  
    64.1 --- a/src/HOL/Induct/Common_Patterns.thy	Tue Sep 09 17:51:07 2014 +0200
    64.2 +++ b/src/HOL/Induct/Common_Patterns.thy	Tue Sep 09 20:51:36 2014 +0200
    64.3 @@ -218,7 +218,7 @@
    64.4    before!
    64.5  *}
    64.6  
    64.7 -datatype foo = Foo1 nat | Foo2 bar
    64.8 +datatype_new foo = Foo1 nat | Foo2 bar
    64.9    and bar = Bar1 bool | Bar2 bazar
   64.10    and bazar = Bazar foo
   64.11  
    65.1 --- a/src/HOL/Induct/Ordinals.thy	Tue Sep 09 17:51:07 2014 +0200
    65.2 +++ b/src/HOL/Induct/Ordinals.thy	Tue Sep 09 20:51:36 2014 +0200
    65.3 @@ -14,7 +14,7 @@
    65.4    @{url "http://www.dcs.ed.ac.uk/home/pgh/chat.html"}).
    65.5  *}
    65.6  
    65.7 -datatype ordinal =
    65.8 +datatype_new ordinal =
    65.9      Zero
   65.10    | Succ ordinal
   65.11    | Limit "nat => ordinal"
    66.1 --- a/src/HOL/Induct/PropLog.thy	Tue Sep 09 17:51:07 2014 +0200
    66.2 +++ b/src/HOL/Induct/PropLog.thy	Tue Sep 09 20:51:36 2014 +0200
    66.3 @@ -20,7 +20,7 @@
    66.4  
    66.5  subsection {* The datatype of propositions *}
    66.6  
    66.7 -datatype 'a pl =
    66.8 +datatype_new 'a pl =
    66.9    false |
   66.10    var 'a ("#_" [1000]) |
   66.11    imp "'a pl" "'a pl" (infixr "->" 90)
    67.1 --- a/src/HOL/Induct/Term.thy	Tue Sep 09 17:51:07 2014 +0200
    67.2 +++ b/src/HOL/Induct/Term.thy	Tue Sep 09 20:51:36 2014 +0200
    67.3 @@ -8,7 +8,7 @@
    67.4  imports Main
    67.5  begin
    67.6  
    67.7 -datatype ('a, 'b) "term" =
    67.8 +datatype_new ('a, 'b) "term" =
    67.9      Var 'a
   67.10    | App 'b "('a, 'b) term list"
   67.11  
    68.1 --- a/src/HOL/Induct/Tree.thy	Tue Sep 09 17:51:07 2014 +0200
    68.2 +++ b/src/HOL/Induct/Tree.thy	Tue Sep 09 20:51:36 2014 +0200
    68.3 @@ -9,7 +9,7 @@
    68.4  imports Main
    68.5  begin
    68.6  
    68.7 -datatype 'a tree =
    68.8 +datatype_new 'a tree =
    68.9      Atom 'a
   68.10    | Branch "nat => 'a tree"
   68.11  
   68.12 @@ -34,7 +34,7 @@
   68.13  
   68.14  subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
   68.15  
   68.16 -datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
   68.17 +datatype_new brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
   68.18  
   68.19  text{*Addition of ordinals*}
   68.20  primrec add :: "[brouwer,brouwer] => brouwer"
    69.1 --- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Sep 09 17:51:07 2014 +0200
    69.2 +++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Sep 09 20:51:36 2014 +0200
    69.3 @@ -31,7 +31,7 @@
    69.4    consisting of variables, constants, and binary operations on
    69.5    expressions. *}
    69.6  
    69.7 -datatype ('adr, 'val) expr =
    69.8 +datatype_new ('adr, 'val) expr =
    69.9      Variable 'adr
   69.10    | Constant 'val
   69.11    | Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
   69.12 @@ -51,7 +51,7 @@
   69.13  text {* Next we model a simple stack machine, with three
   69.14    instructions. *}
   69.15  
   69.16 -datatype ('adr, 'val) instr =
   69.17 +datatype_new ('adr, 'val) instr =
   69.18      Const 'val
   69.19    | Load 'adr
   69.20    | Apply "'val binop"
    70.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Tue Sep 09 17:51:07 2014 +0200
    70.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Tue Sep 09 20:51:36 2014 +0200
    70.3 @@ -21,7 +21,7 @@
    70.4  type_synonym 'a bexp = "'a set"
    70.5  type_synonym 'a assn = "'a set"
    70.6  
    70.7 -datatype 'a com =
    70.8 +datatype_new 'a com =
    70.9      Basic "'a \<Rightarrow> 'a"
   70.10    | Seq "'a com" "'a com"    ("(_;/ _)" [60, 61] 60)
   70.11    | Cond "'a bexp" "'a com" "'a com"
    71.1 --- a/src/HOL/Isar_Examples/Nested_Datatype.thy	Tue Sep 09 17:51:07 2014 +0200
    71.2 +++ b/src/HOL/Isar_Examples/Nested_Datatype.thy	Tue Sep 09 20:51:36 2014 +0200
    71.3 @@ -6,7 +6,7 @@
    71.4  
    71.5  subsection {* Terms and substitution *}
    71.6  
    71.7 -datatype ('a, 'b) "term" =
    71.8 +datatype_new ('a, 'b) "term" =
    71.9    Var 'a
   71.10  | App 'b "('a, 'b) term list"
   71.11  
    72.1 --- a/src/HOL/Lattice/Orders.thy	Tue Sep 09 17:51:07 2014 +0200
    72.2 +++ b/src/HOL/Lattice/Orders.thy	Tue Sep 09 20:51:36 2014 +0200
    72.3 @@ -46,7 +46,7 @@
    72.4    of the original one.
    72.5  *}
    72.6  
    72.7 -datatype 'a dual = dual 'a
    72.8 +datatype_new 'a dual = dual 'a
    72.9  
   72.10  primrec undual :: "'a dual \<Rightarrow> 'a" where
   72.11    undual_dual: "undual (dual x) = x"
    73.1 --- a/src/HOL/Library/Extended.thy	Tue Sep 09 17:51:07 2014 +0200
    73.2 +++ b/src/HOL/Library/Extended.thy	Tue Sep 09 20:51:36 2014 +0200
    73.3 @@ -10,7 +10,7 @@
    73.4    "~~/src/HOL/Library/Simps_Case_Conv"
    73.5  begin
    73.6  
    73.7 -datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
    73.8 +datatype_new 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
    73.9  
   73.10  
   73.11  instantiation extended :: (order)order
    74.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Sep 09 17:51:07 2014 +0200
    74.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Sep 09 20:51:36 2014 +0200
    74.3 @@ -20,7 +20,7 @@
    74.4  
    74.5  subsection {* Definition and basic properties *}
    74.6  
    74.7 -datatype ereal = ereal real | PInfty | MInfty
    74.8 +datatype_new ereal = ereal real | PInfty | MInfty
    74.9  
   74.10  instantiation ereal :: uminus
   74.11  begin
    75.1 --- a/src/HOL/Library/IArray.thy	Tue Sep 09 17:51:07 2014 +0200
    75.2 +++ b/src/HOL/Library/IArray.thy	Tue Sep 09 20:51:36 2014 +0200
    75.3 @@ -13,7 +13,7 @@
    75.4  lists first. Arrays could be converted back into lists for printing if they
    75.5  were wrapped up in an additional constructor. *}
    75.6  
    75.7 -datatype 'a iarray = IArray "'a list"
    75.8 +datatype_new 'a iarray = IArray "'a list"
    75.9  
   75.10  primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
   75.11  "list_of (IArray xs) = xs"
    76.1 --- a/src/HOL/Library/Lattice_Constructions.thy	Tue Sep 09 17:51:07 2014 +0200
    76.2 +++ b/src/HOL/Library/Lattice_Constructions.thy	Tue Sep 09 20:51:36 2014 +0200
    76.3 @@ -9,7 +9,7 @@
    76.4  
    76.5  subsection {* Values extended by a bottom element *}
    76.6  
    76.7 -datatype 'a bot = Value 'a | Bot
    76.8 +datatype_new 'a bot = Value 'a | Bot
    76.9  
   76.10  instantiation bot :: (preorder) preorder
   76.11  begin
   76.12 @@ -108,7 +108,7 @@
   76.13  
   76.14  section {* Values extended by a top element *}
   76.15  
   76.16 -datatype 'a top = Value 'a | Top
   76.17 +datatype_new 'a top = Value 'a | Top
   76.18  
   76.19  instantiation top :: (preorder) preorder
   76.20  begin
   76.21 @@ -207,7 +207,7 @@
   76.22  
   76.23  subsection {* Values extended by a top and a bottom element *}
   76.24  
   76.25 -datatype 'a flat_complete_lattice = Value 'a | Bot | Top
   76.26 +datatype_new 'a flat_complete_lattice = Value 'a | Bot | Top
   76.27  
   76.28  instantiation flat_complete_lattice :: (type) order
   76.29  begin
    77.1 --- a/src/HOL/Library/Parallel.thy	Tue Sep 09 17:51:07 2014 +0200
    77.2 +++ b/src/HOL/Library/Parallel.thy	Tue Sep 09 20:51:36 2014 +0200
    77.3 @@ -8,7 +8,7 @@
    77.4  
    77.5  subsection {* Futures *}
    77.6  
    77.7 -datatype 'a future = fork "unit \<Rightarrow> 'a"
    77.8 +datatype_new 'a future = fork "unit \<Rightarrow> 'a"
    77.9  
   77.10  primrec join :: "'a future \<Rightarrow> 'a" where
   77.11    "join (fork f) = f ()"
    78.1 --- a/src/HOL/Library/Phantom_Type.thy	Tue Sep 09 17:51:07 2014 +0200
    78.2 +++ b/src/HOL/Library/Phantom_Type.thy	Tue Sep 09 20:51:36 2014 +0200
    78.3 @@ -8,7 +8,7 @@
    78.4  imports Main
    78.5  begin
    78.6  
    78.7 -datatype ('a, 'b) phantom = phantom 'b
    78.8 +datatype_new ('a, 'b) phantom = phantom 'b
    78.9  
   78.10  primrec of_phantom :: "('a, 'b) phantom \<Rightarrow> 'b" 
   78.11  where "of_phantom (phantom x) = x"
    79.1 --- a/src/HOL/Library/RBT_Impl.thy	Tue Sep 09 17:51:07 2014 +0200
    79.2 +++ b/src/HOL/Library/RBT_Impl.thy	Tue Sep 09 20:51:36 2014 +0200
    79.3 @@ -16,8 +16,8 @@
    79.4  
    79.5  subsection {* Datatype of RB trees *}
    79.6  
    79.7 -datatype color = R | B
    79.8 -datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
    79.9 +datatype_new color = R | B
   79.10 +datatype_new ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
   79.11  
   79.12  lemma rbt_cases:
   79.13    obtains (Empty) "t = Empty" 
   79.14 @@ -1728,7 +1728,7 @@
   79.15  where
   79.16    "skip_black t = (let t' = skip_red t in case t' of Branch color.B l k v r \<Rightarrow> l | _ \<Rightarrow> t')"
   79.17  
   79.18 -datatype compare = LT | GT | EQ
   79.19 +datatype_new compare = LT | GT | EQ
   79.20  
   79.21  partial_function (tailrec) compare_height :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> compare"
   79.22  where
    80.1 --- a/src/HOL/Metis_Examples/Binary_Tree.thy	Tue Sep 09 17:51:07 2014 +0200
    80.2 +++ b/src/HOL/Metis_Examples/Binary_Tree.thy	Tue Sep 09 20:51:36 2014 +0200
    80.3 @@ -13,7 +13,7 @@
    80.4  
    80.5  declare [[metis_new_skolem]]
    80.6  
    80.7 -datatype 'a bt =
    80.8 +datatype_new 'a bt =
    80.9      Lf
   80.10    | Br 'a  "'a bt"  "'a bt"
   80.11  
    81.1 --- a/src/HOL/Metis_Examples/Message.thy	Tue Sep 09 17:51:07 2014 +0200
    81.2 +++ b/src/HOL/Metis_Examples/Message.thy	Tue Sep 09 20:51:36 2014 +0200
    81.3 @@ -34,10 +34,10 @@
    81.4  definition symKeys :: "key set" where
    81.5    "symKeys == {K. invKey K = K}"
    81.6  
    81.7 -datatype  --{*We allow any number of friendly agents*}
    81.8 +datatype_new  --{*We allow any number of friendly agents*}
    81.9    agent = Server | Friend nat | Spy
   81.10  
   81.11 -datatype
   81.12 +datatype_new
   81.13       msg = Agent  agent     --{*Agent names*}
   81.14           | Number nat       --{*Ordinary integers, timestamps, ...*}
   81.15           | Nonce  nat       --{*Unguessable nonces*}
    82.1 --- a/src/HOL/Metis_Examples/Trans_Closure.thy	Tue Sep 09 17:51:07 2014 +0200
    82.2 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Tue Sep 09 20:51:36 2014 +0200
    82.3 @@ -15,7 +15,7 @@
    82.4  
    82.5  type_synonym addr = nat
    82.6  
    82.7 -datatype val
    82.8 +datatype_new val
    82.9    = Unit        -- "dummy result value of void expressions"
   82.10    | Null        -- "null reference"
   82.11    | Bool bool   -- "Boolean value"
    83.1 --- a/src/HOL/MicroJava/DFA/Err.thy	Tue Sep 09 17:51:07 2014 +0200
    83.2 +++ b/src/HOL/MicroJava/DFA/Err.thy	Tue Sep 09 20:51:36 2014 +0200
    83.3 @@ -9,7 +9,7 @@
    83.4  imports Semilat
    83.5  begin
    83.6  
    83.7 -datatype 'a err = Err | OK 'a
    83.8 +datatype_new 'a err = Err | OK 'a
    83.9  
   83.10  type_synonym 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
   83.11  type_synonym 'a esl = "'a set * 'a ord * 'a ebinop"
    84.1 --- a/src/HOL/MicroJava/J/Example.thy	Tue Sep 09 17:51:07 2014 +0200
    84.2 +++ b/src/HOL/MicroJava/J/Example.thy	Tue Sep 09 20:51:36 2014 +0200
    84.3 @@ -36,8 +36,8 @@
    84.4  \end{verbatim}
    84.5  *}
    84.6  
    84.7 -datatype cnam' = Base' | Ext'
    84.8 -datatype vnam' = vee' | x' | e'
    84.9 +datatype_new cnam' = Base' | Ext'
   84.10 +datatype_new vnam' = vee' | x' | e'
   84.11  
   84.12  text {*
   84.13    @{text cnam'} and @{text vnam'} are intended to be isomorphic 
    85.1 --- a/src/HOL/MicroJava/J/Term.thy	Tue Sep 09 17:51:07 2014 +0200
    85.2 +++ b/src/HOL/MicroJava/J/Term.thy	Tue Sep 09 20:51:36 2014 +0200
    85.3 @@ -6,9 +6,9 @@
    85.4  
    85.5  theory Term imports Value begin
    85.6  
    85.7 -datatype binop = Eq | Add    -- "function codes for binary operation"
    85.8 +datatype_new binop = Eq | Add    -- "function codes for binary operation"
    85.9  
   85.10 -datatype expr
   85.11 +datatype_new expr
   85.12    = NewC cname               -- "class instance creation"
   85.13    | Cast cname expr          -- "type cast"
   85.14    | Lit val                  -- "literal value, also references"
   85.15 @@ -21,7 +21,7 @@
   85.16    | Call cname expr mname 
   85.17      "ty list" "expr list"    ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call" 
   85.18  
   85.19 -datatype stmt
   85.20 +datatype_new stmt
   85.21    = Skip                     -- "empty statement"
   85.22    | Expr expr                -- "expression statement"
   85.23    | Comp stmt stmt       ("_;; _"             [61,60]60)
    86.1 --- a/src/HOL/MicroJava/J/Type.thy	Tue Sep 09 17:51:07 2014 +0200
    86.2 +++ b/src/HOL/MicroJava/J/Type.thy	Tue Sep 09 20:51:36 2014 +0200
    86.3 @@ -45,14 +45,14 @@
    86.4  end
    86.5  
    86.6   -- "exceptions"
    86.7 -datatype 
    86.8 +datatype_new 
    86.9    xcpt   
   86.10    = NullPointer
   86.11    | ClassCast
   86.12    | OutOfMemory
   86.13  
   86.14  -- "class names"
   86.15 -datatype cname  
   86.16 +datatype_new cname  
   86.17    = Object 
   86.18    | Xcpt xcpt 
   86.19    | Cname cnam 
   86.20 @@ -128,23 +128,23 @@
   86.21  end
   86.22  
   86.23  -- "names for @{text This} pointer and local/field variables"
   86.24 -datatype vname 
   86.25 +datatype_new vname 
   86.26    = This
   86.27    | VName vnam
   86.28  
   86.29  -- "primitive type, cf. 4.2"
   86.30 -datatype prim_ty 
   86.31 +datatype_new prim_ty 
   86.32    = Void          -- "'result type' of void methods"
   86.33    | Boolean
   86.34    | Integer
   86.35  
   86.36  -- "reference type, cf. 4.3"
   86.37 -datatype ref_ty   
   86.38 +datatype_new ref_ty   
   86.39    = NullT         -- "null type, cf. 4.1"
   86.40    | ClassT cname  -- "class type"
   86.41  
   86.42  -- "any type, cf. 4.1"
   86.43 -datatype ty 
   86.44 +datatype_new ty 
   86.45    = PrimT prim_ty -- "primitive type"
   86.46    | RefT  ref_ty  -- "reference type"
   86.47  
    87.1 --- a/src/HOL/MicroJava/J/Value.thy	Tue Sep 09 17:51:07 2014 +0200
    87.2 +++ b/src/HOL/MicroJava/J/Value.thy	Tue Sep 09 20:51:36 2014 +0200
    87.3 @@ -8,11 +8,11 @@
    87.4  
    87.5  typedecl loc' -- "locations, i.e. abstract references on objects" 
    87.6  
    87.7 -datatype loc 
    87.8 +datatype_new loc 
    87.9    = XcptRef xcpt -- "special locations for pre-allocated system exceptions"
   87.10    | Loc loc'     -- "usual locations (references on objects)"
   87.11  
   87.12 -datatype val
   87.13 +datatype_new val
   87.14    = Unit        -- "dummy result value of void methods"
   87.15    | Null        -- "null reference"
   87.16    | Bool bool   -- "Boolean value"
    88.1 --- a/src/HOL/MicroJava/JVM/JVMDefensive.thy	Tue Sep 09 17:51:07 2014 +0200
    88.2 +++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy	Tue Sep 09 20:51:36 2014 +0200
    88.3 @@ -11,7 +11,7 @@
    88.4  text {*
    88.5    Extend the state space by one element indicating a type error (or
    88.6    other abnormal termination) *}
    88.7 -datatype 'a type_error = TypeError | Normal 'a
    88.8 +datatype_new 'a type_error = TypeError | Normal 'a
    88.9  
   88.10  
   88.11  abbreviation
    89.1 --- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Tue Sep 09 17:51:07 2014 +0200
    89.2 +++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Tue Sep 09 20:51:36 2014 +0200
    89.3 @@ -8,7 +8,7 @@
    89.4  theory JVMInstructions imports JVMState begin
    89.5  
    89.6  
    89.7 -datatype 
    89.8 +datatype_new 
    89.9    instr = Load nat                  -- "load from local variable"
   89.10          | Store nat                 -- "store into local variable"
   89.11          | LitPush val               -- "push a literal (constant)"
    90.1 --- a/src/HOL/NanoJava/Decl.thy	Tue Sep 09 17:51:07 2014 +0200
    90.2 +++ b/src/HOL/NanoJava/Decl.thy	Tue Sep 09 20:51:36 2014 +0200
    90.3 @@ -7,7 +7,7 @@
    90.4  
    90.5  theory Decl imports Term begin
    90.6  
    90.7 -datatype ty
    90.8 +datatype_new ty
    90.9    = NT           --{* null type  *}
   90.10    | Class cname  --{* class type *}
   90.11  
    91.1 --- a/src/HOL/NanoJava/State.thy	Tue Sep 09 17:51:07 2014 +0200
    91.2 +++ b/src/HOL/NanoJava/State.thy	Tue Sep 09 20:51:36 2014 +0200
    91.3 @@ -13,7 +13,7 @@
    91.4  text {* Locations, i.e.\ abstract references to objects *}
    91.5  typedecl loc 
    91.6  
    91.7 -datatype val
    91.8 +datatype_new val
    91.9    = Null        --{* null reference *}
   91.10    | Addr loc    --{* address, i.e. location of object *}
   91.11  
    92.1 --- a/src/HOL/NanoJava/Term.thy	Tue Sep 09 17:51:07 2014 +0200
    92.2 +++ b/src/HOL/NanoJava/Term.thy	Tue Sep 09 20:51:36 2014 +0200
    92.3 @@ -23,7 +23,7 @@
    92.4    Res_neq_This [simp]: "Res \<noteq> This"
    92.5  *)
    92.6  
    92.7 -datatype stmt
    92.8 +datatype_new stmt
    92.9    = Skip                   --{* empty statement *}
   92.10    | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
   92.11    | Cond expr  stmt stmt   ("If '(_') _ Else _" [ 3,91,91] 91)
    93.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Tue Sep 09 17:51:07 2014 +0200
    93.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Tue Sep 09 20:51:36 2014 +0200
    93.3 @@ -44,7 +44,7 @@
    93.4  nitpick [card = 17, expect = none]
    93.5  oops
    93.6  
    93.7 -datatype ('a, 'b) pd = Pd "'a \<times> 'b"
    93.8 +datatype_new ('a, 'b) pd = Pd "'a \<times> 'b"
    93.9  
   93.10  fun fs where
   93.11  "fs (Pd (a, _)) = a"
   93.12 @@ -76,7 +76,7 @@
   93.13  nitpick [expect = genuine]
   93.14  oops
   93.15  
   93.16 -datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
   93.17 +datatype_new ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
   93.18  
   93.19  fun app where
   93.20  "app (Fn f) x = f x"
    94.1 --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy	Tue Sep 09 17:51:07 2014 +0200
    94.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy	Tue Sep 09 20:51:36 2014 +0200
    94.3 @@ -206,7 +206,7 @@
    94.4  nitpick [binary_ints, expect = none]
    94.5  sorry
    94.6  
    94.7 -datatype tree = Null | Node nat tree tree
    94.8 +datatype_new tree = Null | Node nat tree tree
    94.9  
   94.10  primrec labels where
   94.11  "labels Null = {}" |
    95.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Sep 09 17:51:07 2014 +0200
    95.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Sep 09 20:51:36 2014 +0200
    95.3 @@ -223,7 +223,7 @@
    95.4  
    95.5  subsection {* 2.10. Boxing *}
    95.6  
    95.7 -datatype tm = Var nat | Lam tm | App tm tm
    95.8 +datatype_new tm = Var nat | Lam tm | App tm tm
    95.9  
   95.10  primrec lift where
   95.11  "lift (Var j) k = Var (if j < k then j else j + 1)" |
   95.12 @@ -306,7 +306,7 @@
   95.13  
   95.14  subsection {* 3.1. A Context-Free Grammar *}
   95.15  
   95.16 -datatype alphabet = a | b
   95.17 +datatype_new alphabet = a | b
   95.18  
   95.19  inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
   95.20    "[] \<in> S\<^sub>1"
   95.21 @@ -381,7 +381,7 @@
   95.22  
   95.23  subsection {* 3.2. AA Trees *}
   95.24  
   95.25 -datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
   95.26 +datatype_new 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
   95.27  
   95.28  primrec data where
   95.29  "data \<Lambda> = undefined" |
    96.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue Sep 09 17:51:07 2014 +0200
    96.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Tue Sep 09 20:51:36 2014 +0200
    96.3 @@ -617,7 +617,7 @@
    96.4  
    96.5  text {* Non-recursive datatypes *}
    96.6  
    96.7 -datatype T1 = A | B
    96.8 +datatype_new T1 = A | B
    96.9  
   96.10  lemma "P (x\<Colon>T1)"
   96.11  nitpick [expect = genuine]
   96.12 @@ -653,7 +653,7 @@
   96.13  nitpick [expect = genuine]
   96.14  oops
   96.15  
   96.16 -datatype 'a T2 = C T1 | D 'a
   96.17 +datatype_new 'a T2 = C T1 | D 'a
   96.18  
   96.19  lemma "P (x\<Colon>'a T2)"
   96.20  nitpick [expect = genuine]
   96.21 @@ -685,7 +685,7 @@
   96.22  nitpick [expect = genuine]
   96.23  oops
   96.24  
   96.25 -datatype ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
   96.26 +datatype_new ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
   96.27  
   96.28  lemma "P (x\<Colon>('a, 'b) T3)"
   96.29  nitpick [expect = genuine]
   96.30 @@ -790,7 +790,7 @@
   96.31  nitpick [expect = genuine]
   96.32  oops
   96.33  
   96.34 -datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
   96.35 +datatype_new BitList = BitListNil | Bit0 BitList | Bit1 BitList
   96.36  
   96.37  lemma "P (x\<Colon>BitList)"
   96.38  nitpick [expect = genuine]
   96.39 @@ -823,7 +823,7 @@
   96.40  nitpick [expect = genuine]
   96.41  oops
   96.42  
   96.43 -datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
   96.44 +datatype_new 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
   96.45  
   96.46  lemma "P (x\<Colon>'a BinTree)"
   96.47  nitpick [expect = genuine]
   96.48 @@ -857,7 +857,7 @@
   96.49  
   96.50  text {* Mutually recursive datatypes *}
   96.51  
   96.52 -datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
   96.53 +datatype_new 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
   96.54   and 'a bexp = Equal "'a aexp" "'a aexp"
   96.55  
   96.56  lemma "P (x\<Colon>'a aexp)"
   96.57 @@ -880,17 +880,17 @@
   96.58  nitpick [expect = genuine]
   96.59  oops
   96.60  
   96.61 -lemma "rec_aexp_bexp_1 number ite equal (Number x) = number x"
   96.62 +lemma "rec_aexp number ite equal (Number x) = number x"
   96.63  nitpick [card = 1-3, expect = none]
   96.64  apply simp
   96.65  done
   96.66  
   96.67 -lemma "rec_aexp_bexp_1 number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp_bexp_1 number ite equal y) (rec_aexp_bexp_1 number ite equal z)"
   96.68 +lemma "rec_aexp number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp number ite equal y) (rec_aexp number ite equal z)"
   96.69  nitpick [card = 1-3, expect = none]
   96.70  apply simp
   96.71  done
   96.72  
   96.73 -lemma "P (rec_aexp_bexp_1 number ite equal x)"
   96.74 +lemma "P (rec_aexp number ite equal x)"
   96.75  nitpick [expect = genuine]
   96.76  oops
   96.77  
   96.78 @@ -898,7 +898,7 @@
   96.79  nitpick [expect = genuine]
   96.80  oops
   96.81  
   96.82 -lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp_bexp_1 number ite equal x) (rec_aexp_bexp_1 number ite equal y)"
   96.83 +lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)"
   96.84  nitpick [card = 1-3, expect = none]
   96.85  apply simp
   96.86  done
   96.87 @@ -911,8 +911,7 @@
   96.88  nitpick [expect = genuine]
   96.89  oops
   96.90  
   96.91 -datatype X = A | B X | C Y
   96.92 -     and Y = D X | E Y | F
   96.93 +datatype_new X = A | B X | C Y and Y = D X | E Y | F
   96.94  
   96.95  lemma "P (x\<Colon>X)"
   96.96  nitpick [expect = genuine]
   96.97 @@ -958,22 +957,22 @@
   96.98  nitpick [expect = genuine]
   96.99  oops
  96.100  
  96.101 -lemma "rec_X_Y_1 a b c d e f A = a"
  96.102 +lemma "rec_X a b c d e f A = a"
  96.103  nitpick [card = 1-5, expect = none]
  96.104  apply simp
  96.105  done
  96.106  
  96.107 -lemma "rec_X_Y_1 a b c d e f (B x) = b x (rec_X_Y_1 a b c d e f x)"
  96.108 +lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)"
  96.109  nitpick [card = 1-5, expect = none]
  96.110  apply simp
  96.111  done
  96.112  
  96.113 -lemma "rec_X_Y_1 a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)"
  96.114 +lemma "rec_X a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)"
  96.115  nitpick [card = 1-5, expect = none]
  96.116  apply simp
  96.117  done
  96.118  
  96.119 -lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X_Y_1 a b c d e f x)"
  96.120 +lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X a b c d e f x)"
  96.121  nitpick [card = 1-5, expect = none]
  96.122  apply simp
  96.123  done
  96.124 @@ -988,7 +987,7 @@
  96.125  apply simp
  96.126  done
  96.127  
  96.128 -lemma "P (rec_X_Y_1 a b c d e f x)"
  96.129 +lemma "P (rec_X a b c d e f x)"
  96.130  nitpick [expect = genuine]
  96.131  oops
  96.132  
  96.133 @@ -1000,7 +999,7 @@
  96.134  
  96.135  text {* Indirect recursion is implemented via mutual recursion. *}
  96.136  
  96.137 -datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
  96.138 +datatype_new XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
  96.139  
  96.140  lemma "P (x\<Colon>XOpt)"
  96.141  nitpick [expect = genuine]
  96.142 @@ -1014,12 +1013,12 @@
  96.143  nitpick [expect = genuine]
  96.144  oops
  96.145  
  96.146 -lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
  96.147 +lemma "rec_X cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
  96.148  nitpick [card = 1-5, expect = none]
  96.149  apply simp
  96.150  done
  96.151  
  96.152 -lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))"
  96.153 +lemma "rec_X cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))"
  96.154  nitpick [card = 1-3, expect = none]
  96.155  apply simp
  96.156  done
  96.157 @@ -1029,7 +1028,7 @@
  96.158  apply simp
  96.159  done
  96.160  
  96.161 -lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
  96.162 +lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_X cx dx n1 s1 n2 s2 x)"
  96.163  nitpick [card = 1-4, expect = none]
  96.164  apply simp
  96.165  done
  96.166 @@ -1039,12 +1038,12 @@
  96.167  apply simp
  96.168  done
  96.169  
  96.170 -lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
  96.171 +lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_X cx dx n1 s1 n2 s2 x)"
  96.172  nitpick [card = 1-4, expect = none]
  96.173  apply simp
  96.174  done
  96.175  
  96.176 -lemma "P (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
  96.177 +lemma "P (rec_X cx dx n1 s1 n2 s2 x)"
  96.178  nitpick [expect = genuine]
  96.179  oops
  96.180  
  96.181 @@ -1056,7 +1055,7 @@
  96.182  nitpick [expect = genuine]
  96.183  oops
  96.184  
  96.185 -datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
  96.186 +datatype_new 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
  96.187  
  96.188  lemma "P (x\<Colon>'a YOpt)"
  96.189  nitpick [expect = genuine]
  96.190 @@ -1070,30 +1069,7 @@
  96.191  nitpick [expect = genuine]
  96.192  oops
  96.193  
  96.194 -lemma "rec_YOpt_1 cy n s (CY x) = cy x (rec_YOpt_2 cy n s x)"
  96.195 -nitpick [card = 1-2, expect = none]
  96.196 -apply simp
  96.197 -done
  96.198 -
  96.199 -lemma "rec_YOpt_2 cy n s None = n"
  96.200 -nitpick [card = 1-2, expect = none]
  96.201 -apply simp
  96.202 -done
  96.203 -
  96.204 -lemma "rec_YOpt_2 cy n s (Some x) = s x (\<lambda>a. rec_YOpt_1 cy n s (x a))"
  96.205 -nitpick [card = 1-2, expect = none]
  96.206 -apply simp
  96.207 -done
  96.208 -
  96.209 -lemma "P (rec_YOpt_1 cy n s x)"
  96.210 -nitpick [expect = genuine]
  96.211 -oops
  96.212 -
  96.213 -lemma "P (rec_YOpt_2 cy n s x)"
  96.214 -nitpick [expect = genuine]
  96.215 -oops
  96.216 -
  96.217 -datatype Trie = TR "Trie list"
  96.218 +datatype_new Trie = TR "Trie list"
  96.219  
  96.220  lemma "P (x\<Colon>Trie)"
  96.221  nitpick [expect = genuine]
  96.222 @@ -1107,30 +1083,7 @@
  96.223  nitpick [expect = genuine]
  96.224  oops
  96.225  
  96.226 -lemma "rec_Trie_1 tr nil cons (TR x) = tr x (rec_Trie_2 tr nil cons x)"
  96.227 -nitpick [card = 1-4, expect = none]
  96.228 -apply simp
  96.229 -done
  96.230 -
  96.231 -lemma "rec_Trie_2 tr nil cons [] = nil"
  96.232 -nitpick [card = 1-4, expect = none]
  96.233 -apply simp
  96.234 -done
  96.235 -
  96.236 -lemma "rec_Trie_2 tr nil cons (x#xs) = cons x xs (rec_Trie_1 tr nil cons x) (rec_Trie_2 tr nil cons xs)"
  96.237 -nitpick [card = 1-4, expect = none]
  96.238 -apply simp
  96.239 -done
  96.240 -
  96.241 -lemma "P (rec_Trie_1 tr nil cons x)"
  96.242 -nitpick [card = 1, expect = genuine]
  96.243 -oops
  96.244 -
  96.245 -lemma "P (rec_Trie_2 tr nil cons x)"
  96.246 -nitpick [card = 1, expect = genuine]
  96.247 -oops
  96.248 -
  96.249 -datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
  96.250 +datatype_new InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
  96.251  
  96.252  lemma "P (x\<Colon>InfTree)"
  96.253  nitpick [expect = genuine]
  96.254 @@ -1158,7 +1111,7 @@
  96.255  nitpick [expect = genuine]
  96.256  oops
  96.257  
  96.258 -datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
  96.259 +datatype_new 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
  96.260  
  96.261  lemma "P (x\<Colon>'a lambda)"
  96.262  nitpick [expect = genuine]
  96.263 @@ -1194,8 +1147,8 @@
  96.264  
  96.265  text {* Taken from "Inductive datatypes in HOL", p. 8: *}
  96.266  
  96.267 -datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
  96.268 -datatype 'c U = E "('c, 'c U) T"
  96.269 +datatype_new ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
  96.270 +datatype_new 'c U = E "('c, 'c U) T"
  96.271  
  96.272  lemma "P (x\<Colon>'c U)"
  96.273  nitpick [expect = genuine]
  96.274 @@ -1209,43 +1162,6 @@
  96.275  nitpick [expect = genuine]
  96.276  oops
  96.277  
  96.278 -lemma "rec_U_1 e c d nil cons (E x) = e x (rec_U_2 e c d nil cons x)"
  96.279 -nitpick [card = 1-3, expect = none]
  96.280 -apply simp
  96.281 -done
  96.282 -
  96.283 -lemma "rec_U_2 e c d nil cons (C x) = c x"
  96.284 -nitpick [card = 1-3, expect = none]
  96.285 -apply simp
  96.286 -done
  96.287 -
  96.288 -lemma "rec_U_2 e c d nil cons (D x) = d x (rec_U_3 e c d nil cons x)"
  96.289 -nitpick [card = 1-3, expect = none]
  96.290 -apply simp
  96.291 -done
  96.292 -
  96.293 -lemma "rec_U_3 e c d nil cons [] = nil"
  96.294 -nitpick [card = 1-3, expect = none]
  96.295 -apply simp
  96.296 -done
  96.297 -
  96.298 -lemma "rec_U_3 e c d nil cons (x#xs) = cons x xs (rec_U_1 e c d nil cons x) (rec_U_3 e c d nil cons xs)"
  96.299 -nitpick [card = 1-3, expect = none]
  96.300 -apply simp
  96.301 -done
  96.302 -
  96.303 -lemma "P (rec_U_1 e c d nil cons x)"
  96.304 -nitpick [expect = genuine]
  96.305 -oops
  96.306 -
  96.307 -lemma "P (rec_U_2 e c d nil cons x)"
  96.308 -nitpick [card = 1, expect = genuine]
  96.309 -oops
  96.310 -
  96.311 -lemma "P (rec_U_3 e c d nil cons x)"
  96.312 -nitpick [card = 1, expect = genuine]
  96.313 -oops
  96.314 -
  96.315  subsubsection {* Records *}
  96.316  
  96.317  record ('a, 'b) point =
    97.1 --- a/src/HOL/Nominal/Examples/CK_Machine.thy	Tue Sep 09 17:51:07 2014 +0200
    97.2 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Tue Sep 09 20:51:36 2014 +0200
    97.3 @@ -81,7 +81,7 @@
    97.4  
    97.5  section {* Evaluation Contexts *}
    97.6  
    97.7 -datatype ctx = 
    97.8 +datatype_new ctx = 
    97.9      Hole ("\<box>")  
   97.10    | CAPPL "ctx" "lam"
   97.11    | CAPPR "lam" "ctx"
    98.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Tue Sep 09 17:51:07 2014 +0200
    98.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Tue Sep 09 20:51:36 2014 +0200
    98.3 @@ -38,7 +38,7 @@
    98.4  where
    98.5    "\<lambda>x:T. t \<equiv> Abs T x t"
    98.6  
    98.7 -datatype pat =
    98.8 +datatype_new pat =
    98.9      PVar name ty
   98.10    | PTuple pat pat  ("(1'\<langle>\<langle>_,/ _'\<rangle>\<rangle>)")
   98.11  
    99.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Tue Sep 09 17:51:07 2014 +0200
    99.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Tue Sep 09 20:51:36 2014 +0200
    99.3 @@ -107,7 +107,7 @@
    99.4  
    99.5  hide_const Pow
    99.6  
    99.7 -datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
    99.8 +datatype_new expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
    99.9    | Minus expr expr | Uminus expr | Pow expr int | Exp expr
   99.10  
   99.11  text {*
   99.12 @@ -197,7 +197,7 @@
   99.13  
   99.14  section {* Example negation *}
   99.15  
   99.16 -datatype abc = A | B | C
   99.17 +datatype_new abc = A | B | C
   99.18  
   99.19  inductive notB :: "abc => bool"
   99.20  where
   100.1 --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Sep 09 17:51:07 2014 +0200
   100.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Tue Sep 09 20:51:36 2014 +0200
   100.3 @@ -24,7 +24,7 @@
   100.4      (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
   100.5  *}
   100.6  
   100.7 -datatype alphabet = a | b
   100.8 +datatype_new alphabet = a | b
   100.9  
  100.10  inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
  100.11    "[] \<in> S\<^sub>1"
   101.1 --- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Tue Sep 09 17:51:07 2014 +0200
   101.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Tue Sep 09 20:51:36 2014 +0200
   101.3 @@ -10,11 +10,11 @@
   101.4  
   101.5  text {* a contribution by Aditi Barthwal *}
   101.6  
   101.7 -datatype ('nts,'ts) symbol = NTS 'nts
   101.8 +datatype_new ('nts,'ts) symbol = NTS 'nts
   101.9                              | TS 'ts
  101.10  
  101.11                              
  101.12 -datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"
  101.13 +datatype_new ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"
  101.14  
  101.15  type_synonym ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts"
  101.16  
  101.17 @@ -75,7 +75,7 @@
  101.18  
  101.19  subsection {* Some concrete Context Free Grammars *}
  101.20  
  101.21 -datatype alphabet = a | b
  101.22 +datatype_new alphabet = a | b
  101.23  
  101.24  inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
  101.25    "[] \<in> S\<^sub>1"
  101.26 @@ -140,7 +140,7 @@
  101.27  type_synonym var = nat
  101.28  type_synonym state = "int list"
  101.29  
  101.30 -datatype com =
  101.31 +datatype_new com =
  101.32    Skip |
  101.33    Ass var "state => int" |
  101.34    Seq com com |
  101.35 @@ -164,11 +164,11 @@
  101.36  
  101.37  subsection {* Lambda *}
  101.38  
  101.39 -datatype type =
  101.40 +datatype_new type =
  101.41      Atom nat
  101.42    | Fun type type    (infixr "\<Rightarrow>" 200)
  101.43  
  101.44 -datatype dB =
  101.45 +datatype_new dB =
  101.46      Var nat
  101.47    | App dB dB (infixl "\<degree>" 200)
  101.48    | Abs type dB
  101.49 @@ -237,12 +237,12 @@
  101.50  type_synonym vvalue = int
  101.51  type_synonym var_assign = "vname \<Rightarrow> vvalue"  --"variable assignment"
  101.52  
  101.53 -datatype ir_expr = 
  101.54 +datatype_new ir_expr = 
  101.55    IrConst vvalue
  101.56  | ObjAddr vname
  101.57  | Add ir_expr ir_expr
  101.58  
  101.59 -datatype val =
  101.60 +datatype_new val =
  101.61    IntVal  vvalue
  101.62  
  101.63  record  configuration =
  101.64 @@ -267,14 +267,14 @@
  101.65  type_synonym name = nat --"For simplicity in examples"
  101.66  type_synonym state' = "name \<Rightarrow> nat"
  101.67  
  101.68 -datatype aexp = N nat | V name | Plus aexp aexp
  101.69 +datatype_new aexp = N nat | V name | Plus aexp aexp
  101.70  
  101.71  fun aval :: "aexp \<Rightarrow> state' \<Rightarrow> nat" where
  101.72  "aval (N n) _ = n" |
  101.73  "aval (V x) st = st x" |
  101.74  "aval (Plus e\<^sub>1 e\<^sub>2) st = aval e\<^sub>1 st + aval e\<^sub>2 st"
  101.75  
  101.76 -datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
  101.77 +datatype_new bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
  101.78  
  101.79  primrec bval :: "bexp \<Rightarrow> state' \<Rightarrow> bool" where
  101.80  "bval (B b) _ = b" |
  101.81 @@ -282,7 +282,7 @@
  101.82  "bval (And b1 b2) st = (bval b1 st \<and> bval b2 st)" |
  101.83  "bval (Less a\<^sub>1 a\<^sub>2) st = (aval a\<^sub>1 st < aval a\<^sub>2 st)"
  101.84  
  101.85 -datatype
  101.86 +datatype_new
  101.87    com' = SKIP 
  101.88        | Assign name aexp         ("_ ::= _" [1000, 61] 61)
  101.89        | Semi   com'  com'          ("_; _"  [60, 61] 60)
  101.90 @@ -326,7 +326,7 @@
  101.91  text{* This example formalizes finite CCS processes without communication or
  101.92  recursion. For simplicity, labels are natural numbers. *}
  101.93  
  101.94 -datatype proc = nil | pre nat proc | or proc proc | par proc proc
  101.95 +datatype_new proc = nil | pre nat proc | or proc proc | par proc proc
  101.96  
  101.97  inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
  101.98  "step (pre n p) n p" |
   102.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Sep 09 17:51:07 2014 +0200
   102.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Sep 09 20:51:36 2014 +0200
   102.3 @@ -2,13 +2,13 @@
   102.4  imports Main
   102.5  begin
   102.6  
   102.7 -datatype guest = Guest0 | Guest1
   102.8 -datatype key = Key0 | Key1 | Key2 | Key3
   102.9 -datatype room = Room0
  102.10 +datatype_new guest = Guest0 | Guest1
  102.11 +datatype_new key = Key0 | Key1 | Key2 | Key3
  102.12 +datatype_new room = Room0
  102.13  
  102.14  type_synonym card = "key * key"
  102.15  
  102.16 -datatype event =
  102.17 +datatype_new event =
  102.18     Check_in guest room card | Enter guest room card | Exit guest room
  102.19  
  102.20  definition initk :: "room \<Rightarrow> key"
   103.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Tue Sep 09 17:51:07 2014 +0200
   103.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Tue Sep 09 20:51:36 2014 +0200
   103.3 @@ -11,7 +11,7 @@
   103.4  type_synonym var = unit
   103.5  type_synonym state = bool
   103.6  
   103.7 -datatype com =
   103.8 +datatype_new com =
   103.9    Skip |
  103.10    Ass bool |
  103.11    Seq com com |
   104.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Tue Sep 09 17:51:07 2014 +0200
   104.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Tue Sep 09 20:51:36 2014 +0200
   104.3 @@ -11,7 +11,7 @@
   104.4  type_synonym var = unit
   104.5  type_synonym state = bool
   104.6  
   104.7 -datatype com =
   104.8 +datatype_new com =
   104.9    Skip |
  104.10    Ass bool |
  104.11    Seq com com |
   105.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Tue Sep 09 17:51:07 2014 +0200
   105.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Tue Sep 09 20:51:36 2014 +0200
   105.3 @@ -11,7 +11,7 @@
   105.4  type_synonym var = unit
   105.5  type_synonym state = int
   105.6  
   105.7 -datatype com =
   105.8 +datatype_new com =
   105.9    Skip |
  105.10    Ass var "int" |
  105.11    Seq com com |
   106.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Tue Sep 09 17:51:07 2014 +0200
   106.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Tue Sep 09 20:51:36 2014 +0200
   106.3 @@ -11,7 +11,7 @@
   106.4  type_synonym var = nat
   106.5  type_synonym state = "int list"
   106.6  
   106.7 -datatype com =
   106.8 +datatype_new com =
   106.9    Skip |
  106.10    Ass var "int" |
  106.11    Seq com com |
   107.1 --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Sep 09 17:51:07 2014 +0200
   107.2 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Sep 09 20:51:36 2014 +0200
   107.3 @@ -4,11 +4,11 @@
   107.4  
   107.5  subsection {* Lambda *}
   107.6  
   107.7 -datatype type =
   107.8 +datatype_new type =
   107.9      Atom nat
  107.10    | Fun type type    (infixr "\<Rightarrow>" 200)
  107.11  
  107.12 -datatype dB =
  107.13 +datatype_new dB =
  107.14      Var nat
  107.15    | App dB dB (infixl "\<degree>" 200)
  107.16    | Abs type dB
   108.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Sep 09 17:51:07 2014 +0200
   108.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Sep 09 20:51:36 2014 +0200
   108.3 @@ -53,7 +53,7 @@
   108.4  
   108.5  section {* Context Free Grammar *}
   108.6  
   108.7 -datatype alphabet = a | b
   108.8 +datatype_new alphabet = a | b
   108.9  
  108.10  inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
  108.11    "[] \<in> S\<^sub>1"
  108.12 @@ -179,7 +179,7 @@
  108.13  type_synonym var = nat
  108.14  type_synonym state = "int list"
  108.15  
  108.16 -datatype com =
  108.17 +datatype_new com =
  108.18    Skip |
  108.19    Ass var "int" |
  108.20    Seq com com |
  108.21 @@ -206,11 +206,11 @@
  108.22  
  108.23  subsection {* Lambda *}
  108.24  
  108.25 -datatype type =
  108.26 +datatype_new type =
  108.27      Atom nat
  108.28    | Fun type type    (infixr "\<Rightarrow>" 200)
  108.29  
  108.30 -datatype dB =
  108.31 +datatype_new dB =
  108.32      Var nat
  108.33    | App dB dB (infixl "\<degree>" 200)
  108.34    | Abs type dB
   109.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Sep 09 17:51:07 2014 +0200
   109.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Sep 09 20:51:36 2014 +0200
   109.3 @@ -139,7 +139,7 @@
   109.4  
   109.5  subsection {* Alternative Rules *}
   109.6  
   109.7 -datatype char = C | D | E | F | G | H
   109.8 +datatype_new char = C | D | E | F | G | H
   109.9  
  109.10  inductive is_C_or_D
  109.11  where
  109.12 @@ -784,7 +784,7 @@
  109.13  type_synonym var = nat
  109.14  type_synonym state = "int list"
  109.15  
  109.16 -datatype com =
  109.17 +datatype_new com =
  109.18    Skip |
  109.19    Ass var "state => int" |
  109.20    Seq com com |
  109.21 @@ -809,7 +809,7 @@
  109.22  text{* This example formalizes finite CCS processes without communication or
  109.23  recursion. For simplicity, labels are natural numbers. *}
  109.24  
  109.25 -datatype proc = nil | pre nat proc | or proc proc | par proc proc
  109.26 +datatype_new proc = nil | pre nat proc | or proc proc | par proc proc
  109.27  
  109.28  inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
  109.29  where
  109.30 @@ -974,7 +974,7 @@
  109.31  *)
  109.32  subsection {* AVL Tree *}
  109.33  
  109.34 -datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
  109.35 +datatype_new 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
  109.36  fun height :: "'a tree => nat" where
  109.37  "height ET = 0"
  109.38  | "height (MKT x l r h) = max (height l) (height r) + 1"
  109.39 @@ -1403,7 +1403,7 @@
  109.40  
  109.41  thm is_error'.equation
  109.42  
  109.43 -datatype ErrorObject = Error String.literal int
  109.44 +datatype_new ErrorObject = Error String.literal int
  109.45  
  109.46  inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
  109.47  where
  109.48 @@ -1508,7 +1508,7 @@
  109.49  
  109.50  text {* The higher-order predicate r is in an output term *}
  109.51  
  109.52 -datatype result = Result bool
  109.53 +datatype_new result = Result bool
  109.54  
  109.55  inductive fixed_relation :: "'a => bool"
  109.56  
   110.1 --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Tue Sep 09 17:51:07 2014 +0200
   110.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Tue Sep 09 20:51:36 2014 +0200
   110.3 @@ -9,7 +9,7 @@
   110.4    manually slightly adapted.
   110.5  *}
   110.6   
   110.7 -datatype Nat = Zer
   110.8 +datatype_new Nat = Zer
   110.9               | Suc Nat
  110.10  
  110.11  fun sub :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat"
  110.12 @@ -20,10 +20,10 @@
  110.13                                           Zer \<Rightarrow> Zer
  110.14                                         | Suc x' \<Rightarrow> sub x' y')"
  110.15  
  110.16 -datatype Sym = N0
  110.17 +datatype_new Sym = N0
  110.18               | N1 Sym
  110.19  
  110.20 -datatype RE = Sym Sym
  110.21 +datatype_new RE = Sym Sym
  110.22              | Or RE RE
  110.23              | Seq RE RE
  110.24              | And RE RE
   111.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Sep 09 17:51:07 2014 +0200
   111.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Sep 09 20:51:36 2014 +0200
   111.3 @@ -107,13 +107,13 @@
   111.4    "unique [] = True"
   111.5  | "unique (x # xs) = (xs\<langle>fst x\<rangle>\<^sub>? = \<bottom> \<and> unique xs)"
   111.6  
   111.7 -datatype type =
   111.8 +datatype_new type =
   111.9      TVar nat
  111.10    | Top
  111.11    | Fun type type    (infixr "\<rightarrow>" 200)
  111.12    | TyAll type type  ("(3\<forall><:_./ _)" [0, 10] 10)
  111.13  
  111.14 -datatype binding = VarB type | TVarB type
  111.15 +datatype_new binding = VarB type | TVarB type
  111.16  type_synonym env = "binding list"
  111.17  
  111.18  primrec is_TVarB :: "binding \<Rightarrow> bool"
  111.19 @@ -131,7 +131,7 @@
  111.20    "mapB f (VarB T) = VarB (f T)"
  111.21  | "mapB f (TVarB T) = TVarB (f T)"
  111.22  
  111.23 -datatype trm =
  111.24 +datatype_new trm =
  111.25      Var nat
  111.26    | Abs type trm   ("(3\<lambda>:_./ _)" [0, 10] 10)
  111.27    | TAbs type trm  ("(3\<lambda><:_./ _)" [0, 10] 10)
   112.1 --- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Tue Sep 09 17:51:07 2014 +0200
   112.2 +++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Tue Sep 09 20:51:36 2014 +0200
   112.3 @@ -2,7 +2,7 @@
   112.4  imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
   112.5  begin
   112.6  
   112.7 -datatype agent = Alice | Bob | Spy
   112.8 +datatype_new agent = Alice | Bob | Spy
   112.9  
  112.10  definition agents :: "agent set"
  112.11  where
  112.12 @@ -12,14 +12,14 @@
  112.13  where
  112.14    "bad = {Spy}"
  112.15  
  112.16 -datatype key = pubEK agent | priEK agent
  112.17 +datatype_new key = pubEK agent | priEK agent
  112.18  
  112.19  fun invKey
  112.20  where
  112.21    "invKey (pubEK A) = priEK A"
  112.22  | "invKey (priEK A) = pubEK A"
  112.23  
  112.24 -datatype
  112.25 +datatype_new
  112.26       msg = Agent  agent
  112.27           | Key    key
  112.28           | Nonce  nat
  112.29 @@ -73,7 +73,7 @@
  112.30  | initState_Spy:
  112.31      "initState Spy        =  (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)"
  112.32  
  112.33 -datatype
  112.34 +datatype_new
  112.35    event = Says  agent agent msg
  112.36          | Gets  agent       msg
  112.37          | Notes agent       msg
   113.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Tue Sep 09 17:51:07 2014 +0200
   113.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Tue Sep 09 20:51:36 2014 +0200
   113.3 @@ -18,7 +18,7 @@
   113.4  
   113.5  subsection {* The Binary Tree *}
   113.6  
   113.7 -datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip
   113.8 +datatype_new 'a tree = Node "'a tree" 'a bool "'a tree" | Tip
   113.9  
  113.10  
  113.11  text {* The boolean flag in the node marks the content of the node as
   114.1 --- a/src/HOL/TLA/Inc/Inc.thy	Tue Sep 09 17:51:07 2014 +0200
   114.2 +++ b/src/HOL/TLA/Inc/Inc.thy	Tue Sep 09 20:51:36 2014 +0200
   114.3 @@ -9,7 +9,7 @@
   114.4  begin
   114.5  
   114.6  (* program counter as an enumeration type *)
   114.7 -datatype pcount = a | b | g
   114.8 +datatype_new pcount = a | b | g
   114.9  
  114.10  axiomatization
  114.11    (* program variables *)
   115.1 --- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Tue Sep 09 17:51:07 2014 +0200
   115.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Tue Sep 09 20:51:36 2014 +0200
   115.3 @@ -8,7 +8,7 @@
   115.4  imports RPCParameters
   115.5  begin
   115.6  
   115.7 -datatype mClkState = clkA | clkB
   115.8 +datatype_new mClkState = clkA | clkB
   115.9  
  115.10  (* types sent on the clerk's send and receive channels are argument types
  115.11     of the memory and the RPC, respectively *)
   116.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Sep 09 17:51:07 2014 +0200
   116.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Tue Sep 09 20:51:36 2014 +0200
   116.3 @@ -8,7 +8,7 @@
   116.4  imports Memory RPC MemClerk
   116.5  begin
   116.6  
   116.7 -datatype histState = histA | histB
   116.8 +datatype_new histState = histA | histB
   116.9  
  116.10  type_synonym histType = "(PrIds => histState) stfun"  (* the type of the history variable *)
  116.11  
   117.1 --- a/src/HOL/TLA/Memory/MemoryParameters.thy	Tue Sep 09 17:51:07 2014 +0200
   117.2 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Tue Sep 09 20:51:36 2014 +0200
   117.3 @@ -9,7 +9,7 @@
   117.4  begin
   117.5  
   117.6  (* the memory operations *)
   117.7 -datatype memOp = read Locs | "write" Locs Vals
   117.8 +datatype_new memOp = read Locs | "write" Locs Vals
   117.9  
  117.10  consts
  117.11    (* memory locations and contents *)
   118.1 --- a/src/HOL/TLA/Memory/RPCParameters.thy	Tue Sep 09 17:51:07 2014 +0200
   118.2 +++ b/src/HOL/TLA/Memory/RPCParameters.thy	Tue Sep 09 20:51:36 2014 +0200
   118.3 @@ -13,8 +13,8 @@
   118.4    memory implementation.
   118.5  *)
   118.6  
   118.7 -datatype rpcOp = memcall memOp | othercall Vals
   118.8 -datatype rpcState = rpcA | rpcB
   118.9 +datatype_new rpcOp = memcall memOp | othercall Vals
  118.10 +datatype_new rpcState = rpcA | rpcB
  118.11  
  118.12  consts
  118.13    (* some particular return values *)
   119.1 --- a/src/HOL/UNITY/Comp/Counter.thy	Tue Sep 09 17:51:07 2014 +0200
   119.2 +++ b/src/HOL/UNITY/Comp/Counter.thy	Tue Sep 09 20:51:36 2014 +0200
   119.3 @@ -13,7 +13,7 @@
   119.4  theory Counter imports "../UNITY_Main" begin
   119.5  
   119.6  (* Variables are names *)
   119.7 -datatype name = C | c nat
   119.8 +datatype_new name = C | c nat
   119.9  type_synonym state = "name=>int"
  119.10  
  119.11  primrec sum  :: "[nat,state]=>int" where
   120.1 --- a/src/HOL/UNITY/Simple/Network.thy	Tue Sep 09 17:51:07 2014 +0200
   120.2 +++ b/src/HOL/UNITY/Simple/Network.thy	Tue Sep 09 20:51:36 2014 +0200
   120.3 @@ -11,9 +11,9 @@
   120.4  
   120.5  (*The state assigns a number to each process variable*)
   120.6  
   120.7 -datatype pvar = Sent | Rcvd | Idle
   120.8 +datatype_new pvar = Sent | Rcvd | Idle
   120.9  
  120.10 -datatype pname = Aproc | Bproc
  120.11 +datatype_new pname = Aproc | Bproc
  120.12  
  120.13  type_synonym state = "pname * pvar => nat"
  120.14  
   121.1 --- a/src/HOL/UNITY/Simple/Token.thy	Tue Sep 09 17:51:07 2014 +0200
   121.2 +++ b/src/HOL/UNITY/Simple/Token.thy	Tue Sep 09 20:51:36 2014 +0200
   121.3 @@ -15,7 +15,7 @@
   121.4  
   121.5  subsection{*Definitions*}
   121.6  
   121.7 -datatype pstate = Hungry | Eating | Thinking
   121.8 +datatype_new pstate = Hungry | Eating | Thinking
   121.9      --{*process states*}
  121.10  
  121.11  record state =
   122.1 --- a/src/HOL/Unix/Nested_Environment.thy	Tue Sep 09 17:51:07 2014 +0200
   122.2 +++ b/src/HOL/Unix/Nested_Environment.thy	Tue Sep 09 20:51:36 2014 +0200
   122.3 @@ -19,7 +19,7 @@
   122.4    position within the structure.
   122.5  *}
   122.6  
   122.7 -datatype ('a, 'b, 'c) env =
   122.8 +datatype_new ('a, 'b, 'c) env =
   122.9      Val 'a
  122.10    | Env 'b  "'c \<Rightarrow> ('a, 'b, 'c) env option"
  122.11  
   123.1 --- a/src/HOL/Unix/Unix.thy	Tue Sep 09 17:51:07 2014 +0200
   123.2 +++ b/src/HOL/Unix/Unix.thy	Tue Sep 09 20:51:36 2014 +0200
   123.3 @@ -73,7 +73,7 @@
   123.4    \cite{Naraschewski:2001}.}
   123.5  *}
   123.6  
   123.7 -datatype perm =
   123.8 +datatype_new perm =
   123.9      Readable
  123.10    | Writable
  123.11    | Executable    -- "(ignored)"
  123.12 @@ -284,7 +284,7 @@
  123.13    @{text "root \<midarrow>x\<rightarrow> root'"} for the operational semantics.
  123.14  *}
  123.15  
  123.16 -datatype operation =
  123.17 +datatype_new operation =
  123.18      Read uid string path
  123.19    | Write uid string path
  123.20    | Chmod uid perms path
   124.1 --- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Tue Sep 09 17:51:07 2014 +0200
   124.2 +++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Tue Sep 09 20:51:36 2014 +0200
   124.3 @@ -19,7 +19,7 @@
   124.4  subsection {* Plain Ad Hoc Overloading *}
   124.5  
   124.6  text {*Consider the type of first-order terms.*}
   124.7 -datatype ('a, 'b) "term" =
   124.8 +datatype_new ('a, 'b) "term" =
   124.9    Var 'b |
  124.10    Fun 'a "('a, 'b) term list"
  124.11  
   125.1 --- a/src/HOL/ex/BT.thy	Tue Sep 09 17:51:07 2014 +0200
   125.2 +++ b/src/HOL/ex/BT.thy	Tue Sep 09 20:51:36 2014 +0200
   125.3 @@ -9,7 +9,7 @@
   125.4  
   125.5  theory BT imports Main begin
   125.6  
   125.7 -datatype 'a bt =
   125.8 +datatype_new 'a bt =
   125.9      Lf
  125.10    | Br 'a  "'a bt"  "'a bt"
  125.11  
   126.1 --- a/src/HOL/ex/Chinese.thy	Tue Sep 09 17:51:07 2014 +0200
   126.2 +++ b/src/HOL/ex/Chinese.thy	Tue Sep 09 20:51:36 2014 +0200
   126.3 @@ -16,7 +16,7 @@
   126.4  
   126.5      *}
   126.6  
   126.7 -datatype shuzi =
   126.8 +datatype_new shuzi =
   126.9      One   ("一")
  126.10    | Two   ("二")
  126.11    | Three ("三") 
   127.1 --- a/src/HOL/ex/Eval_Examples.thy	Tue Sep 09 17:51:07 2014 +0200
   127.2 +++ b/src/HOL/ex/Eval_Examples.thy	Tue Sep 09 20:51:36 2014 +0200
   127.3 @@ -42,7 +42,7 @@
   127.4  
   127.5  text {* a fancy datatype *}
   127.6  
   127.7 -datatype ('a, 'b) foo =
   127.8 +datatype_new ('a, 'b) foo =
   127.9      Foo "'a\<Colon>order" 'b
  127.10    | Bla "('a, 'b) bar"
  127.11    | Dummy nat
   128.1 --- a/src/HOL/ex/Fundefs.thy	Tue Sep 09 17:51:07 2014 +0200
   128.2 +++ b/src/HOL/ex/Fundefs.thy	Tue Sep 09 20:51:36 2014 +0200
   128.3 @@ -372,7 +372,7 @@
   128.4  
   128.5  
   128.6  (* Simple Higher-Order Recursion *)
   128.7 -datatype 'a tree = 
   128.8 +datatype_new 'a tree = 
   128.9    Leaf 'a 
  128.10    | Branch "'a tree list"
  128.11  
  128.12 @@ -423,7 +423,7 @@
  128.13  
  128.14  
  128.15  (* Many equations (quadratic blowup) *)
  128.16 -datatype DT = 
  128.17 +datatype_new DT = 
  128.18    A | B | C | D | E | F | G | H | I | J | K | L | M | N | P
  128.19  | Q | R | S | T | U | V
  128.20  
   129.1 --- a/src/HOL/ex/Hebrew.thy	Tue Sep 09 17:51:07 2014 +0200
   129.2 +++ b/src/HOL/ex/Hebrew.thy	Tue Sep 09 20:51:36 2014 +0200
   129.3 @@ -12,7 +12,7 @@
   129.4  
   129.5  text {* The Hebrew Alef-Bet (א-ב). *}
   129.6  
   129.7 -datatype alef_bet =
   129.8 +datatype_new alef_bet =
   129.9      Alef    ("א")
  129.10    | Bet     ("ב")
  129.11    | Gimel   ("ג")
   130.1 --- a/src/HOL/ex/Normalization_by_Evaluation.thy	Tue Sep 09 17:51:07 2014 +0200
   130.2 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Tue Sep 09 20:51:36 2014 +0200
   130.3 @@ -15,7 +15,7 @@
   130.4  lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
   130.5  lemma "~((0::nat) < (0::nat))" by normalization
   130.6  
   130.7 -datatype n = Z | S n
   130.8 +datatype_new n = Z | S n
   130.9  
  130.10  primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where
  130.11     "add Z = id"
   131.1 --- a/src/HOL/ex/Records.thy	Tue Sep 09 17:51:07 2014 +0200
   131.2 +++ b/src/HOL/ex/Records.thy	Tue Sep 09 20:51:36 2014 +0200
   131.3 @@ -166,7 +166,7 @@
   131.4  
   131.5  subsection {* Coloured points: record extension *}
   131.6  
   131.7 -datatype colour = Red | Green | Blue
   131.8 +datatype_new colour = Red | Green | Blue
   131.9  
  131.10  record cpoint = point +
  131.11    colour :: colour
   132.1 --- a/src/HOL/ex/Reflection_Examples.thy	Tue Sep 09 17:51:07 2014 +0200
   132.2 +++ b/src/HOL/ex/Reflection_Examples.thy	Tue Sep 09 20:51:36 2014 +0200
   132.3 @@ -46,7 +46,7 @@
   132.4  text {* Example 1 : Propositional formulae and NNF. *}
   132.5  text {* The type @{text fm} represents simple propositional formulae: *}
   132.6  
   132.7 -datatype form = TrueF | FalseF | Less nat nat
   132.8 +datatype_new form = TrueF | FalseF | Less nat nat
   132.9    | And form form | Or form form | Neg form | ExQ form
  132.10  
  132.11  primrec interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool"
  132.12 @@ -66,7 +66,7 @@
  132.13    apply reify
  132.14    oops
  132.15  
  132.16 -datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
  132.17 +datatype_new fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
  132.18  
  132.19  primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
  132.20  where
  132.21 @@ -135,7 +135,7 @@
  132.22  text {* Example 2: Simple arithmetic formulae *}
  132.23  
  132.24  text {* The type @{text num} reflects linear expressions over natural number *}
  132.25 -datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
  132.26 +datatype_new num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
  132.27  
  132.28  text {* This is just technical to make recursive definitions easier. *}
  132.29  primrec num_size :: "num \<Rightarrow> nat" 
  132.30 @@ -252,7 +252,7 @@
  132.31  
  132.32  text {* Let's lift this to formulae and see what happens *}
  132.33  
  132.34 -datatype aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
  132.35 +datatype_new aform = Lt num num  | Eq num num | Ge num num | NEq num num | 
  132.36    Conj aform aform | Disj aform aform | NEG aform | T | F
  132.37  
  132.38  primrec linaformsize:: "aform \<Rightarrow> nat"
  132.39 @@ -331,7 +331,7 @@
  132.40    one envornement of different types and show that automatic reification also deals with
  132.41    bindings *}
  132.42    
  132.43 -datatype rb = BC bool | BAnd rb rb | BOr rb rb
  132.44 +datatype_new rb = BC bool | BAnd rb rb | BOr rb rb
  132.45  
  132.46  primrec Irb :: "rb \<Rightarrow> bool"
  132.47  where
  132.48 @@ -343,7 +343,7 @@
  132.49    apply (reify Irb.simps)
  132.50  oops
  132.51  
  132.52 -datatype rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
  132.53 +datatype_new rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
  132.54    | INeg rint | ISub rint rint
  132.55  
  132.56  primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
  132.57 @@ -370,7 +370,7 @@
  132.58    apply (reify Irint_simps ("(3::int) * x + y * y - 9 + (- z)"))
  132.59    oops
  132.60  
  132.61 -datatype rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
  132.62 +datatype_new rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
  132.63  
  132.64  primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> int list"
  132.65  where
  132.66 @@ -387,7 +387,7 @@
  132.67    apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs"))
  132.68    oops
  132.69  
  132.70 -datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
  132.71 +datatype_new rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
  132.72    | NNeg rnat | NSub rnat rnat | Nlgth rlist
  132.73  
  132.74  primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> nat list \<Rightarrow> nat"
  132.75 @@ -418,7 +418,7 @@
  132.76       ("Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs)"))
  132.77    oops
  132.78  
  132.79 -datatype rifm = RT | RF | RVar nat
  132.80 +datatype_new rifm = RT | RF | RVar nat
  132.81    | RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat
  132.82    | RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm
  132.83    | RNEX rifm | RIEX rifm | RLEX rifm | RNALL rifm | RIALL rifm | RLALL rifm
  132.84 @@ -451,7 +451,7 @@
  132.85  
  132.86  text {* An example for equations containing type variables *}
  132.87  
  132.88 -datatype prod = Zero | One | Var nat | Mul prod prod 
  132.89 +datatype_new prod = Zero | One | Var nat | Mul prod prod 
  132.90    | Pw prod nat | PNM nat nat prod
  132.91  
  132.92  primrec Iprod :: " prod \<Rightarrow> ('a::linordered_idom) list \<Rightarrow>'a" 
  132.93 @@ -463,7 +463,7 @@
  132.94  | "Iprod (Pw a n) vs = Iprod a vs ^ n"
  132.95  | "Iprod (PNM n k t) vs = (vs ! n) ^ k * Iprod t vs"
  132.96  
  132.97 -datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
  132.98 +datatype_new sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F 
  132.99    | Or sgn sgn | And sgn sgn
 132.100  
 132.101  primrec Isgn :: "sgn \<Rightarrow> ('a::linordered_idom) list \<Rightarrow> bool"
   133.1 --- a/src/HOL/ex/Seq.thy	Tue Sep 09 17:51:07 2014 +0200
   133.2 +++ b/src/HOL/ex/Seq.thy	Tue Sep 09 20:51:36 2014 +0200
   133.3 @@ -8,7 +8,7 @@
   133.4  imports Main
   133.5  begin
   133.6  
   133.7 -datatype 'a seq = Empty | Seq 'a "'a seq"
   133.8 +datatype_new 'a seq = Empty | Seq 'a "'a seq"
   133.9  
  133.10  fun conc :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq"
  133.11  where
   134.1 --- a/src/HOL/ex/Serbian.thy	Tue Sep 09 17:51:07 2014 +0200
   134.2 +++ b/src/HOL/ex/Serbian.thy	Tue Sep 09 20:51:36 2014 +0200
   134.3 @@ -11,7 +11,7 @@
   134.4  begin
   134.5  
   134.6  text{* Serbian cyrillic letters *}
   134.7 -datatype azbuka =
   134.8 +datatype_new azbuka =
   134.9    azbA   ("А")
  134.10  | azbB   ("Б")
  134.11  | azbV   ("В")
  134.12 @@ -47,7 +47,7 @@
  134.13  thm azbuka.induct
  134.14  
  134.15  text{* Serbian latin letters *}
  134.16 -datatype abeceda =
  134.17 +datatype_new abeceda =
  134.18    abcA   ("A")
  134.19  | abcB   ("B")
  134.20  | abcC   ("C")
   135.1 --- a/src/HOL/ex/Termination.thy	Tue Sep 09 17:51:07 2014 +0200
   135.2 +++ b/src/HOL/ex/Termination.thy	Tue Sep 09 20:51:36 2014 +0200
   135.3 @@ -118,7 +118,7 @@
   135.4    
   135.5  subsection {* Simple examples with other datatypes than nat, e.g. trees and lists *}
   135.6  
   135.7 -datatype tree = Node | Branch tree tree
   135.8 +datatype_new tree = Node | Branch tree tree
   135.9  
  135.10  fun g_tree :: "tree * tree \<Rightarrow> tree"
  135.11  where
   136.1 --- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Tue Sep 09 17:51:07 2014 +0200
   136.2 +++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Tue Sep 09 20:51:36 2014 +0200
   136.3 @@ -6,7 +6,7 @@
   136.4  imports "~~/src/HOL/Library/Transitive_Closure_Table"
   136.5  begin
   136.6  
   136.7 -datatype ty = A | B | C
   136.8 +datatype_new ty = A | B | C
   136.9  
  136.10  inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
  136.11  where
   137.1 --- a/src/HOL/ex/Tree23.thy	Tue Sep 09 17:51:07 2014 +0200
   137.2 +++ b/src/HOL/ex/Tree23.thy	Tue Sep 09 20:51:36 2014 +0200
   137.3 @@ -21,16 +21,16 @@
   137.4  
   137.5  type_synonym key = int -- {*for simplicity, should be a type class*}
   137.6  
   137.7 -datatype ord = LESS | EQUAL | GREATER
   137.8 +datatype_new ord = LESS | EQUAL | GREATER
   137.9  
  137.10  definition "ord i j = (if i<j then LESS else if i=j then EQUAL else GREATER)"
  137.11  
  137.12 -datatype 'a tree23 =
  137.13 +datatype_new 'a tree23 =
  137.14    Empty |
  137.15    Branch2 "'a tree23" "key * 'a" "'a tree23" |
  137.16    Branch3 "'a tree23" "key * 'a" "'a tree23" "key * 'a" "'a tree23"
  137.17  
  137.18 -datatype 'a growth =
  137.19 +datatype_new 'a growth =
  137.20    Stay "'a tree23" |
  137.21    Sprout "'a tree23" "key * 'a" "'a tree23"
  137.22  
  137.23 @@ -402,7 +402,7 @@
  137.24  text{* This is a little test harness and should be commented out once the
  137.25  above functions have been proved correct. *}
  137.26  
  137.27 -datatype 'a act = Add int 'a | Del int
  137.28 +datatype_new 'a act = Add int 'a | Del int
  137.29  
  137.30  fun exec where
  137.31  "exec [] t = t" |
   138.1 --- a/src/HOL/ex/Unification.thy	Tue Sep 09 17:51:07 2014 +0200
   138.2 +++ b/src/HOL/ex/Unification.thy	Tue Sep 09 20:51:36 2014 +0200
   138.3 @@ -32,7 +32,7 @@
   138.4  
   138.5  text {* Binary trees with leaves that are constants or variables. *}
   138.6  
   138.7 -datatype 'a trm = 
   138.8 +datatype_new 'a trm = 
   138.9    Var 'a 
  138.10    | Const 'a
  138.11    | Comb "'a trm" "'a trm" (infix "\<cdot>" 60)