renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
authorblanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 5830557752a91eec4
parent 58304 acc2f1801acc
child 58306 117ba6cbe414
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
src/Doc/Codegen/Evaluation.thy
src/Doc/Codegen/Introduction.thy
src/Doc/Codegen/Refinement.thy
src/Doc/Datatypes/Datatypes.thy
src/Doc/Datatypes/document/root.tex
src/Doc/Functions/Functions.thy
src/Doc/Isar_Ref/Generic.thy
src/Doc/Isar_Ref/HOL_Specific.thy
src/Doc/Isar_Ref/Spec.thy
src/Doc/Isar_Ref/Synopsis.thy
src/Doc/Tutorial/CodeGen/CodeGen.thy
src/Doc/Tutorial/Datatype/Fundata.thy
src/Doc/Tutorial/Datatype/Nested.thy
src/Doc/Tutorial/Protocol/Message.thy
src/Doc/Tutorial/Trie/Trie.thy
src/HOL/Auth/Event.thy
src/HOL/Auth/Guard/Extensions.thy
src/HOL/BNF_Examples/Compat.thy
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Datatype_Benchmark/Brackin.thy
src/HOL/Datatype_Benchmark/Instructions.thy
src/HOL/Fun_Def.thy
src/HOL/HOLCF/FOCUS/Buffer.thy
src/HOL/Hoare/Hoare_Logic.thy
src/HOL/Hoare/Hoare_Logic_Abort.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy
src/HOL/IMP/Com.thy
src/HOL/IMP/Procs.thy
src/HOL/Imperative_HOL/Heap.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
src/HOL/Induct/Com.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Induct/SList.thy
src/HOL/Nominal/Examples/Fsub.thy
src/HOL/Old_Datatype.thy
src/HOL/Quotient_Examples/Quotient_Message.thy
src/HOL/SET_Protocol/Event_SET.thy
src/HOL/SET_Protocol/Message_SET.thy
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/ex/Reflection_Examples.thy
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -205,7 +205,7 @@
     1.4    An simplistic example:
     1.5  *}
     1.6  
     1.7 -datatype %quote form_ord = T | F | Less nat nat
     1.8 +datatype_new %quote form_ord = T | F | Less nat nat
     1.9    | And form_ord form_ord | Or form_ord form_ord | Neg form_ord
    1.10  
    1.11  primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
    1.12 @@ -259,7 +259,7 @@
    1.13    example:
    1.14  *}
    1.15  
    1.16 -datatype %quote form = T | F | And form form | Or form form (*<*)
    1.17 +datatype_new %quote form = T | F | And form form | Or form form (*<*)
    1.18  
    1.19  (*>*) ML %quotett {*
    1.20    fun eval_form @{code T} = true
     2.1 --- a/src/Doc/Codegen/Introduction.thy	Thu Sep 11 18:54:36 2014 +0200
     2.2 +++ b/src/Doc/Codegen/Introduction.thy	Thu Sep 11 18:54:36 2014 +0200
     2.3 @@ -35,7 +35,7 @@
     2.4  subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *}
     2.5  
     2.6  text {*
     2.7 -  In a HOL theory, the @{command_def datatype} and @{command_def
     2.8 +  In a HOL theory, the @{command_def datatype_new} and @{command_def
     2.9    definition}/@{command_def primrec}/@{command_def fun} declarations
    2.10    form the core of a functional programming language.  By default
    2.11    equational theorems stemming from those are used for generated code,
    2.12 @@ -45,7 +45,7 @@
    2.13    For example, here a simple \qt{implementation} of amortised queues:
    2.14  *}
    2.15  
    2.16 -datatype %quote 'a queue = AQueue "'a list" "'a list"
    2.17 +datatype_new %quote 'a queue = AQueue "'a list" "'a list"
    2.18  
    2.19  definition %quote empty :: "'a queue" where
    2.20    "empty = AQueue [] []"
     3.1 --- a/src/Doc/Codegen/Refinement.thy	Thu Sep 11 18:54:36 2014 +0200
     3.2 +++ b/src/Doc/Codegen/Refinement.thy	Thu Sep 11 18:54:36 2014 +0200
     3.3 @@ -87,7 +87,7 @@
     3.4    queues:
     3.5  *}
     3.6  
     3.7 -datatype %quote 'a queue = Queue "'a list"
     3.8 +datatype_new %quote 'a queue = Queue "'a list"
     3.9  
    3.10  definition %quote empty :: "'a queue" where
    3.11    "empty = Queue []"
     4.1 --- a/src/Doc/Datatypes/Datatypes.thy	Thu Sep 11 18:54:36 2014 +0200
     4.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 11 18:54:36 2014 +0200
     4.3 @@ -5,7 +5,7 @@
     4.4      Author:     Andrei Popescu, TU Muenchen
     4.5      Author:     Dmitriy Traytel, TU Muenchen
     4.6  
     4.7 -Tutorial for (co)datatype definitions with the new package.
     4.8 +Tutorial for (co)datatype definitions.
     4.9  *)
    4.10  
    4.11  theory Datatypes
    4.12 @@ -21,14 +21,9 @@
    4.13    \label{sec:introduction} *}
    4.14  
    4.15  text {*
    4.16 -The 2013 edition of Isabelle introduced a new definitional package for freely
    4.17 -generated datatypes and codatatypes. The datatype support is similar to that
    4.18 -provided by the earlier package due to Berghofer and Wenzel
    4.19 -\cite{Berghofer-Wenzel:1999:TPHOL}, documented in the Isar reference manual
    4.20 -\cite{isabelle-isar-ref}; indeed, replacing the keyword \keyw{datatype} by
    4.21 -@{command datatype_new} is often all that is needed to port existing theories to
    4.22 -use the new package.
    4.23 -
    4.24 +The 2013 edition of Isabelle introduced a definitional package for freely
    4.25 +generated datatypes and codatatypes. This package replaces the earlier
    4.26 +implementation due to Berghofer and Wenzel \cite{Berghofer-Wenzel:1999:TPHOL}.
    4.27  Perhaps the main advantage of the new package is that it supports recursion
    4.28  through a large class of non-datatypes, such as finite sets:
    4.29  *}
    4.30 @@ -51,7 +46,7 @@
    4.31  generated discriminators, selectors, and relators as well as a wealth of
    4.32  properties about them.
    4.33  
    4.34 -In addition to inductive datatypes, the new package supports coinductive
    4.35 +In addition to inductive datatypes, the package supports coinductive
    4.36  datatypes, or \emph{codatatypes}, which allow infinite values. For example, the
    4.37  following command introduces the type of lazy lists, which comprises both finite
    4.38  and infinite values:
    4.39 @@ -151,12 +146,8 @@
    4.40  \newcommand\authoremailv{\texttt{tray{\color{white}NOSPAM}\kern-\wd\boxA{}tel@\allowbreak
    4.41  in.\allowbreak tum.\allowbreak de}}
    4.42  
    4.43 -The command @{command datatype_new} is expected to replace \keyw{datatype} in a
    4.44 -future release. Authors of new theories are encouraged to use the new commands,
    4.45 -and maintainers of older theories may want to consider upgrading.
    4.46 -
    4.47 -Comments and bug reports concerning either the tool or this tutorial should be
    4.48 -directed to the authors at \authoremaili, \authoremailii, \authoremailiii,
    4.49 +Comments and bug reports concerning either the package or this tutorial should
    4.50 +be directed to the authors at \authoremaili, \authoremailii, \authoremailiii,
    4.51  \authoremailiv, and \authoremailv.
    4.52  *}
    4.53  
    4.54 @@ -1036,8 +1027,9 @@
    4.55  
    4.56  text {*
    4.57  The command @{command datatype_new} has been designed to be highly compatible
    4.58 -with the old \keyw{datatype}, to ease migration. There are nonetheless a few
    4.59 -incompatibilities that may arise when porting to the new package:
    4.60 +with the old command (which is now called \keyw{old_datatype}), to ease
    4.61 +migration. There are nonetheless a few incompatibilities that may arise when
    4.62 +porting:
    4.63  
    4.64  \begin{itemize}
    4.65  \setlength{\itemsep}{0pt}
    4.66 @@ -1065,8 +1057,8 @@
    4.67  @{text "[unfolded all_mem_range]"} attribute on @{text t.induct}.
    4.68  
    4.69  \item \emph{The internal constructions are completely different.} Proof texts
    4.70 -that unfold the definition of constants introduced by \keyw{datatype} will be
    4.71 -difficult to port.
    4.72 +that unfold the definition of constants introduced by \keyw{old\_datatype} will
    4.73 +be difficult to port.
    4.74  
    4.75  \item \emph{Some constants and theorems have different names.}
    4.76  For non-mutually recursive datatypes,
    4.77 @@ -2696,9 +2688,6 @@
    4.78  %  * need for this is rare but may arise if you want e.g. to add destructors to
    4.79  %    a type not introduced by ...
    4.80  %
    4.81 -%  * also useful for compatibility with old package, e.g. add destructors to
    4.82 -%    old \keyw{datatype}
    4.83 -%
    4.84  %  * @{command free_constructors}
    4.85  %    * @{text plugins}, @{text discs_sels}
    4.86  %    * hack to have both co and nonco view via locale (cf. ext nats)
     5.1 --- a/src/Doc/Datatypes/document/root.tex	Thu Sep 11 18:54:36 2014 +0200
     5.2 +++ b/src/Doc/Datatypes/document/root.tex	Thu Sep 11 18:54:36 2014 +0200
     5.3 @@ -76,10 +76,9 @@
     5.4  
     5.5  \begin{abstract}
     5.6  \noindent
     5.7 -This tutorial describes the new package for defining datatypes and codatatypes
     5.8 +This tutorial describes the definitional package for datatypes and codatatypes
     5.9  in Isabelle/HOL. The package provides four main commands: \keyw{datatype_new},
    5.10 -\keyw{codatatype}, \keyw{primrec}, and \keyw{primcorec}. The first command is
    5.11 -expected to eventually replace the old \keyw{datatype} command.
    5.12 +\keyw{codatatype}, \keyw{primrec}, and \keyw{primcorec}.
    5.13  \end{abstract}
    5.14  
    5.15  \tableofcontents
     6.1 --- a/src/Doc/Functions/Functions.thy	Thu Sep 11 18:54:36 2014 +0200
     6.2 +++ b/src/Doc/Functions/Functions.thy	Thu Sep 11 18:54:36 2014 +0200
     6.3 @@ -522,7 +522,7 @@
     6.4    and @{term "X"} for true, false and uncertain propositions, respectively. 
     6.5  *}
     6.6  
     6.7 -datatype P3 = T | F | X
     6.8 +datatype_new P3 = T | F | X
     6.9  
    6.10  text {* \noindent Then the conjunction of such values can be defined as follows: *}
    6.11  
    6.12 @@ -1122,7 +1122,7 @@
    6.13    As an example, imagine a datatype of n-ary trees:
    6.14  *}
    6.15  
    6.16 -datatype 'a tree = 
    6.17 +datatype_new 'a tree = 
    6.18    Leaf 'a 
    6.19  | Branch "'a tree list"
    6.20  
     7.1 --- a/src/Doc/Isar_Ref/Generic.thy	Thu Sep 11 18:54:36 2014 +0200
     7.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Thu Sep 11 18:54:36 2014 +0200
     7.3 @@ -736,7 +736,7 @@
     7.4    monotonically through the theory hierarchy: forming a new theory,
     7.5    the union of the simpsets of its imports are taken as starting
     7.6    point.  Also note that definitional packages like @{command
     7.7 -  "datatype"}, @{command "primrec"}, @{command "fun"} routinely
     7.8 +  "datatype_new"}, @{command "primrec"}, @{command "fun"} routinely
     7.9    declare Simplifier rules to the target context, while plain
    7.10    @{command "definition"} is an exception in \emph{not} declaring
    7.11    anything.
     8.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Sep 11 18:54:36 2014 +0200
     8.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Sep 11 18:54:36 2014 +0200
     8.3 @@ -283,11 +283,10 @@
     8.4    \begin{description}
     8.5  
     8.6    \item @{command (HOL) "primrec"} defines primitive recursive
     8.7 -  functions over datatypes (see also @{command_ref (HOL) datatype} and
     8.8 -  @{command_ref (HOL) rep_datatype}).  The given @{text equations}
     8.9 -  specify reduction rules that are produced by instantiating the
    8.10 -  generic combinator for primitive recursion that is available for
    8.11 -  each datatype.
    8.12 +  functions over datatypes (see also @{command_ref (HOL) datatype_new}).
    8.13 +  The given @{text equations} specify reduction rules that are produced
    8.14 +  by instantiating the generic combinator for primitive recursion that
    8.15 +  is available for each datatype.
    8.16  
    8.17    Each equation needs to be of the form:
    8.18  
    8.19 @@ -379,7 +378,7 @@
    8.20    boolean expressions, and use @{command primrec} for evaluation
    8.21    functions that follow the same recursive structure. *}
    8.22  
    8.23 -datatype 'a aexp =
    8.24 +datatype_new 'a aexp =
    8.25      IF "'a bexp"  "'a aexp"  "'a aexp"
    8.26    | Sum "'a aexp"  "'a aexp"
    8.27    | Diff "'a aexp"  "'a aexp"
    8.28 @@ -450,7 +449,7 @@
    8.29  text {* Functions on datatypes with nested recursion are also defined
    8.30    by mutual primitive recursion. *}
    8.31  
    8.32 -datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
    8.33 +datatype_new ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
    8.34  
    8.35  text {* A substitution function on type @{typ "('a, 'b) term"} can be
    8.36    defined as follows, by working simultaneously on @{typ "('a, 'b)
    8.37 @@ -471,7 +470,7 @@
    8.38  
    8.39  lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)" and
    8.40    "subst_term_list (subst_term f1 \<circ> f2) ts = subst_term_list f1 (subst_term_list f2 ts)"
    8.41 -  by (induct t and ts) simp_all
    8.42 +  by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
    8.43  
    8.44  
    8.45  subsubsection {* Example: a map function for infinitely branching trees *}
    8.46 @@ -480,7 +479,7 @@
    8.47    primitive recursion is just as easy.
    8.48  *}
    8.49  
    8.50 -datatype 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
    8.51 +datatype_new 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
    8.52  
    8.53  primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
    8.54  where
    8.55 @@ -702,16 +701,16 @@
    8.56  *}
    8.57  
    8.58  
    8.59 -section {* Datatypes \label{sec:hol-datatype} *}
    8.60 +section {* Old-style datatypes \label{sec:hol-datatype} *}
    8.61  
    8.62  text {*
    8.63    \begin{matharray}{rcl}
    8.64 -    @{command_def (HOL) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\
    8.65 +    @{command_def (HOL) "old_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
    8.66      @{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
    8.67    \end{matharray}
    8.68  
    8.69    @{rail \<open>
    8.70 -    @@{command (HOL) datatype} (spec + @'and')
    8.71 +    @@{command (HOL) old_datatype} (spec + @'and')
    8.72      ;
    8.73      @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
    8.74      ;
    8.75 @@ -723,30 +722,16 @@
    8.76  
    8.77    \begin{description}
    8.78  
    8.79 -  \item @{command (HOL) "datatype"} defines inductive datatypes in
    8.80 -  HOL.
    8.81 +  \item @{command (HOL) "old_datatype"} defines old-style inductive
    8.82 +  datatypes in HOL.
    8.83  
    8.84    \item @{command (HOL) "rep_datatype"} represents existing types as
    8.85 -  datatypes.
    8.86 -
    8.87 -  For foundational reasons, some basic types such as @{typ nat}, @{typ
    8.88 -  "'a \<times> 'b"}, @{typ "'a + 'b"}, @{typ bool} and @{typ unit} are
    8.89 -  introduced by more primitive means using @{command_ref typedef}.  To
    8.90 -  recover the rich infrastructure of @{command datatype} (e.g.\ rules
    8.91 -  for @{method cases} and @{method induct} and the primitive recursion
    8.92 -  combinators), such types may be represented as actual datatypes
    8.93 -  later.  This is done by specifying the constructors of the desired
    8.94 -  type, and giving a proof of the induction rule, distinctness and
    8.95 -  injectivity of constructors.
    8.96 -
    8.97 -  For example, see @{file "~~/src/HOL/Sum_Type.thy"} for the
    8.98 -  representation of the primitive sum type as fully-featured datatype.
    8.99 +  old-style datatypes.
   8.100  
   8.101    \end{description}
   8.102  
   8.103 -  The generated rules for @{method induct} and @{method cases} provide
   8.104 -  case names according to the given constructors, while parameters are
   8.105 -  named after the types (see also \secref{sec:cases-induct}).
   8.106 +  These commands are mostly obsolete; @{command (HOL) "datatype"}
   8.107 +  should be used instead.
   8.108  
   8.109    See \cite{isabelle-HOL} for more details on datatypes, but beware of
   8.110    the old-style theory syntax being used there!  Apart from proper
   8.111 @@ -764,7 +749,7 @@
   8.112    names than the existing @{typ "'a list"} that is already in @{theory
   8.113    Main}: *}
   8.114  
   8.115 -datatype 'a seq = Empty | Seq 'a "'a seq"
   8.116 +datatype_new 'a seq = Empty | Seq 'a "'a seq"
   8.117  
   8.118  text {* We can now prove some simple lemma by structural induction: *}
   8.119  
   8.120 @@ -1173,9 +1158,9 @@
   8.121    by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject)
   8.122  
   8.123  text {* Note that such trivial constructions are better done with
   8.124 -  derived specification mechanisms such as @{command datatype}: *}
   8.125 -
   8.126 -datatype three' = One' | Two' | Three'
   8.127 +  derived specification mechanisms such as @{command datatype_new}: *}
   8.128 +
   8.129 +datatype_new three' = One' | Two' | Three'
   8.130  
   8.131  text {* This avoids re-doing basic definitions and proofs from the
   8.132    primitive @{command typedef} above. *}
   8.133 @@ -2369,7 +2354,7 @@
   8.134    to reason about inductive types.  Rules are selected according to
   8.135    the declarations by the @{attribute cases} and @{attribute induct}
   8.136    attributes, cf.\ \secref{sec:cases-induct}.  The @{command (HOL)
   8.137 -  datatype} package already takes care of this.
   8.138 +  datatype_new} package already takes care of this.
   8.139  
   8.140    These unstructured tactics feature both goal addressing and dynamic
   8.141    instantiation.  Note that named rule cases are \emph{not} provided
     9.1 --- a/src/Doc/Isar_Ref/Spec.thy	Thu Sep 11 18:54:36 2014 +0200
     9.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Thu Sep 11 18:54:36 2014 +0200
     9.3 @@ -81,7 +81,7 @@
     9.4    the formal text.  Examples may be seen in Isabelle/HOL sources
     9.5    itself, such as @{keyword "keywords"}~@{verbatim "\"typedef\""}
     9.6    @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim
     9.7 -  "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations
     9.8 +  "\"old_datatype\""} @{text ":: thy_decl"} for theory-level declarations
     9.9    with and without proof, respectively.  Additional @{syntax tags}
    9.10    provide defaults for document preparation (\secref{sec:tags}).
    9.11  
    10.1 --- a/src/Doc/Isar_Ref/Synopsis.thy	Thu Sep 11 18:54:36 2014 +0200
    10.2 +++ b/src/Doc/Isar_Ref/Synopsis.thy	Thu Sep 11 18:54:36 2014 +0200
    10.3 @@ -1068,7 +1068,7 @@
    10.4    provide suitable derived cases rules.
    10.5  *}
    10.6  
    10.7 -datatype foo = Foo | Bar foo
    10.8 +datatype_new foo = Foo | Bar foo
    10.9  
   10.10  notepad
   10.11  begin
    11.1 --- a/src/Doc/Tutorial/CodeGen/CodeGen.thy	Thu Sep 11 18:54:36 2014 +0200
    11.2 +++ b/src/Doc/Tutorial/CodeGen/CodeGen.thy	Thu Sep 11 18:54:36 2014 +0200
    11.3 @@ -16,9 +16,9 @@
    11.4  *}
    11.5  
    11.6  type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v";
    11.7 -datatype ('a,'v)expr = Cex 'v
    11.8 -                     | Vex 'a
    11.9 -                     | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr";
   11.10 +datatype (dead 'a, 'v) expr = Cex 'v
   11.11 +                      | Vex 'a
   11.12 +                      | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr";
   11.13  
   11.14  text{*\noindent
   11.15  The three constructors represent constants, variables and the application of
   11.16 @@ -40,7 +40,7 @@
   11.17  the result. As for @{text"expr"}, addresses and values are type parameters:
   11.18  *}
   11.19  
   11.20 -datatype ('a,'v) instr = Const 'v
   11.21 +datatype (dead 'a, 'v) instr = Const 'v
   11.22                         | Load 'a
   11.23                         | Apply "'v binop";
   11.24  
    12.1 --- a/src/Doc/Tutorial/Datatype/Fundata.thy	Thu Sep 11 18:54:36 2014 +0200
    12.2 +++ b/src/Doc/Tutorial/Datatype/Fundata.thy	Thu Sep 11 18:54:36 2014 +0200
    12.3 @@ -1,7 +1,7 @@
    12.4  (*<*)
    12.5  theory Fundata imports Main begin
    12.6  (*>*)
    12.7 -datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
    12.8 +datatype (dead 'a,'i) bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
    12.9  
   12.10  text{*\noindent
   12.11  Parameter @{typ"'a"} is the type of values stored in
    13.1 --- a/src/Doc/Tutorial/Datatype/Nested.thy	Thu Sep 11 18:54:36 2014 +0200
    13.2 +++ b/src/Doc/Tutorial/Datatype/Nested.thy	Thu Sep 11 18:54:36 2014 +0200
    13.3 @@ -67,7 +67,7 @@
    13.4  
    13.5  lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst  Var t  = (t ::('v,'f)term)  \<and>
    13.6                    substs Var ts = (ts::('v,'f)term list)";
    13.7 -apply(induct_tac t and ts, simp_all);
    13.8 +apply(induct_tac t and ts rule: subst.induct substs.induct, simp_all);
    13.9  done
   13.10  
   13.11  text{*\noindent
   13.12 @@ -105,7 +105,7 @@
   13.13  (* Exercise 1: *)
   13.14  lemma "subst  ((subst f) \<circ> g) t  = subst  f (subst g t) \<and>
   13.15         substs ((subst f) \<circ> g) ts = substs f (substs g ts)"
   13.16 -apply (induct_tac t and ts)
   13.17 +apply (induct_tac t and ts rule: subst.induct substs.induct)
   13.18  apply (simp_all)
   13.19  done
   13.20  
   13.21 @@ -125,7 +125,7 @@
   13.22  
   13.23  lemma "trev (trev t) = (t::('v,'f)term) \<and> 
   13.24         trevs (trevs ts) = (ts::('v,'f)term list)"
   13.25 -apply (induct_tac t and ts, simp_all)
   13.26 +apply (induct_tac t and ts rule: trev.induct trevs.induct, simp_all)
   13.27  done
   13.28  (*>*)
   13.29  
    14.1 --- a/src/Doc/Tutorial/Protocol/Message.thy	Thu Sep 11 18:54:36 2014 +0200
    14.2 +++ b/src/Doc/Tutorial/Protocol/Message.thy	Thu Sep 11 18:54:36 2014 +0200
    14.3 @@ -334,6 +334,7 @@
    14.4   txt{*MPair case: blast works out the necessary sum itself!*}
    14.5   prefer 2 apply auto apply (blast elim!: add_leE)
    14.6  txt{*Nonce case*}
    14.7 +apply (rename_tac nat)
    14.8  apply (rule_tac x = "N + Suc nat" in exI, auto) 
    14.9  done
   14.10  (*>*)
    15.1 --- a/src/Doc/Tutorial/Trie/Trie.thy	Thu Sep 11 18:54:36 2014 +0200
    15.2 +++ b/src/Doc/Tutorial/Trie/Trie.thy	Thu Sep 11 18:54:36 2014 +0200
    15.3 @@ -208,7 +208,7 @@
    15.4  
    15.5  
    15.6  (* Exercise 3. Solution by Getrud Bauer *)
    15.7 -datatype ('a,'v) triem = Triem  "'v option" "'a \<Rightarrow> ('a,'v) triem option";
    15.8 +datatype ('a,dead 'v) triem = Triem  "'v option" "'a \<Rightarrow> ('a,'v) triem option";
    15.9  
   15.10  primrec valuem :: "('a, 'v) triem \<Rightarrow> 'v option" where
   15.11  "valuem (Triem ov m) = ov"
    16.1 --- a/src/HOL/Auth/Event.thy	Thu Sep 11 18:54:36 2014 +0200
    16.2 +++ b/src/HOL/Auth/Event.thy	Thu Sep 11 18:54:36 2014 +0200
    16.3 @@ -15,7 +15,7 @@
    16.4  consts  (*Initial states of agents -- parameter of the construction*)
    16.5    initState :: "agent => msg set"
    16.6  
    16.7 -datatype
    16.8 +datatype_new
    16.9    event = Says  agent agent msg
   16.10          | Gets  agent       msg
   16.11          | Notes agent       msg
    17.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Thu Sep 11 18:54:36 2014 +0200
    17.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Thu Sep 11 18:54:36 2014 +0200
    17.3 @@ -579,6 +579,7 @@
    17.4  apply (drule_tac P="%G. X:parts G" in knows_Cons_substD, safe)
    17.5  apply (erule initState_used)
    17.6  apply (case_tac a, auto)
    17.7 +apply (rename_tac msg)
    17.8  apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
    17.9  by (auto dest: Says_imp_used intro: used_ConsI)
   17.10  
   17.11 @@ -592,6 +593,7 @@
   17.12  apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
   17.13  apply (drule_tac P="%G. X:parts G" in knows_max_Cons_substD, safe)
   17.14  apply (case_tac a, auto)
   17.15 +apply (rename_tac msg)
   17.16  apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
   17.17  by (auto simp: knows_max'_Cons dest: Says_imp_used intro: used_ConsI)
   17.18  
    18.1 --- a/src/HOL/BNF_Examples/Compat.thy	Thu Sep 11 18:54:36 2014 +0200
    18.2 +++ b/src/HOL/BNF_Examples/Compat.thy	Thu Sep 11 18:54:36 2014 +0200
    18.3 @@ -27,7 +27,7 @@
    18.4    |> tap (check_lens lens);
    18.5  \<close>
    18.6  
    18.7 -datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst"
    18.8 +old_datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst"
    18.9  
   18.10  ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name old_lst}; \<close>
   18.11  
   18.12 @@ -169,11 +169,11 @@
   18.13  ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo'}; \<close>
   18.14  ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar'}; \<close>
   18.15  
   18.16 -datatype funky = Funky "funky tre" | Funky'
   18.17 +old_datatype funky = Funky "funky tre" | Funky'
   18.18  
   18.19  ML \<open> get_descrs @{theory} (3, 3, 3) @{type_name funky}; \<close>
   18.20  
   18.21 -datatype fnky = Fnky "nat tre"
   18.22 +old_datatype fnky = Fnky "nat tre"
   18.23  
   18.24  ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name fnky}; \<close>
   18.25  
    19.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 11 18:54:36 2014 +0200
    19.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 11 18:54:36 2014 +0200
    19.3 @@ -12,6 +12,7 @@
    19.4  theory BNF_Least_Fixpoint
    19.5  imports BNF_Fixpoint_Base
    19.6  keywords
    19.7 +  "datatype" :: thy_decl and
    19.8    "datatype_new" :: thy_decl and
    19.9    "datatype_compat" :: thy_decl
   19.10  begin
    20.1 --- a/src/HOL/Datatype_Benchmark/Brackin.thy	Thu Sep 11 18:54:36 2014 +0200
    20.2 +++ b/src/HOL/Datatype_Benchmark/Brackin.thy	Thu Sep 11 18:54:36 2014 +0200
    20.3 @@ -5,13 +5,13 @@
    20.4  
    20.5  theory Brackin imports Main begin
    20.6  
    20.7 -datatype T =
    20.8 +old_datatype T =
    20.9      X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
   20.10      X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
   20.11      X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
   20.12      X32 | X33 | X34
   20.13  
   20.14 -datatype ('a, 'b, 'c) TY1 =
   20.15 +old_datatype ('a, 'b, 'c) TY1 =
   20.16        NoF
   20.17      | Fk 'a "('a, 'b, 'c) TY2"
   20.18  and ('a, 'b, 'c) TY2 =
    21.1 --- a/src/HOL/Datatype_Benchmark/Instructions.thy	Thu Sep 11 18:54:36 2014 +0200
    21.2 +++ b/src/HOL/Datatype_Benchmark/Instructions.thy	Thu Sep 11 18:54:36 2014 +0200
    21.3 @@ -5,158 +5,158 @@
    21.4  
    21.5  theory Instructions imports Main begin
    21.6  
    21.7 -datatype Size = Byte | Word | Long
    21.8 +old_datatype Size = Byte | Word | Long
    21.9  
   21.10 -datatype DataRegister
   21.11 -              = RegD0
   21.12 -              | RegD1
   21.13 -              | RegD2
   21.14 -              | RegD3
   21.15 -              | RegD4
   21.16 -              | RegD5
   21.17 -              | RegD6
   21.18 -              | RegD7
   21.19 +old_datatype DataRegister =
   21.20 +  RegD0
   21.21 +| RegD1
   21.22 +| RegD2
   21.23 +| RegD3
   21.24 +| RegD4
   21.25 +| RegD5
   21.26 +| RegD6
   21.27 +| RegD7
   21.28  
   21.29 -datatype AddressRegister
   21.30 -              = RegA0
   21.31 -              | RegA1
   21.32 -              | RegA2
   21.33 -              | RegA3
   21.34 -              | RegA4
   21.35 -              | RegA5
   21.36 -              | RegA6
   21.37 -              | RegA7
   21.38 +old_datatype AddressRegister =
   21.39 +  RegA0
   21.40 +| RegA1
   21.41 +| RegA2
   21.42 +| RegA3
   21.43 +| RegA4
   21.44 +| RegA5
   21.45 +| RegA6
   21.46 +| RegA7
   21.47  
   21.48 -datatype DataOrAddressRegister
   21.49 -              = data DataRegister
   21.50 -              | address AddressRegister
   21.51 +old_datatype DataOrAddressRegister =
   21.52 +  data DataRegister
   21.53 +| address AddressRegister
   21.54  
   21.55 -datatype Condition
   21.56 -              = Hi
   21.57 -              | Ls
   21.58 -              | Cc
   21.59 -              | Cs
   21.60 -              | Ne
   21.61 -              | Eq
   21.62 -              | Vc
   21.63 -              | Vs
   21.64 -              | Pl
   21.65 -              | Mi
   21.66 -              | Ge
   21.67 -              | Lt
   21.68 -              | Gt
   21.69 -              | Le
   21.70 +old_datatype Condition =
   21.71 +  Hi
   21.72 +| Ls
   21.73 +| Cc
   21.74 +| Cs
   21.75 +| Ne
   21.76 +| Eq
   21.77 +| Vc
   21.78 +| Vs
   21.79 +| Pl
   21.80 +| Mi
   21.81 +| Ge
   21.82 +| Lt
   21.83 +| Gt
   21.84 +| Le
   21.85  
   21.86 -datatype AddressingMode
   21.87 -        = immediate nat
   21.88 -        | direct DataOrAddressRegister
   21.89 -        | indirect AddressRegister
   21.90 -        | postinc AddressRegister
   21.91 -        | predec AddressRegister
   21.92 -        | indirectdisp nat AddressRegister
   21.93 -        | indirectindex nat AddressRegister DataOrAddressRegister Size
   21.94 -        | absolute nat
   21.95 -        | pcdisp nat
   21.96 -        | pcindex nat DataOrAddressRegister Size
   21.97 +old_datatype AddressingMode =
   21.98 +  immediate nat
   21.99 +| direct DataOrAddressRegister
  21.100 +| indirect AddressRegister
  21.101 +| postinc AddressRegister
  21.102 +| predec AddressRegister
  21.103 +| indirectdisp nat AddressRegister
  21.104 +| indirectindex nat AddressRegister DataOrAddressRegister Size
  21.105 +| absolute nat
  21.106 +| pcdisp nat
  21.107 +| pcindex nat DataOrAddressRegister Size
  21.108  
  21.109 -datatype M68kInstruction
  21.110 -    = ABCD AddressingMode AddressingMode
  21.111 -    | ADD Size AddressingMode AddressingMode
  21.112 -    | ADDA Size AddressingMode AddressRegister
  21.113 -    | ADDI Size nat AddressingMode
  21.114 -    | ADDQ Size nat AddressingMode
  21.115 -    | ADDX Size AddressingMode AddressingMode
  21.116 -    | AND Size AddressingMode AddressingMode
  21.117 -    | ANDI Size nat AddressingMode
  21.118 -    | ANDItoCCR nat
  21.119 -    | ANDItoSR nat
  21.120 -    | ASL Size AddressingMode DataRegister
  21.121 -    | ASLW AddressingMode
  21.122 -    | ASR Size AddressingMode DataRegister
  21.123 -    | ASRW AddressingMode
  21.124 -    | Bcc Condition Size nat
  21.125 -    | BTST Size AddressingMode AddressingMode
  21.126 -    | BCHG Size AddressingMode AddressingMode
  21.127 -    | BCLR Size AddressingMode AddressingMode
  21.128 -    | BSET Size AddressingMode AddressingMode
  21.129 -    | BRA Size nat
  21.130 -    | BSR Size nat
  21.131 -    | CHK AddressingMode DataRegister
  21.132 -    | CLR Size AddressingMode
  21.133 -    | CMP Size AddressingMode DataRegister
  21.134 -    | CMPA Size AddressingMode AddressRegister
  21.135 -    | CMPI Size nat AddressingMode
  21.136 -    | CMPM Size AddressRegister AddressRegister
  21.137 -    | DBT DataRegister nat
  21.138 -    | DBF DataRegister nat
  21.139 -    | DBcc Condition DataRegister nat
  21.140 -    | DIVS AddressingMode DataRegister
  21.141 -    | DIVU AddressingMode DataRegister
  21.142 -    | EOR Size DataRegister AddressingMode
  21.143 -    | EORI Size nat AddressingMode
  21.144 -    | EORItoCCR nat
  21.145 -    | EORItoSR nat
  21.146 -    | EXG DataOrAddressRegister DataOrAddressRegister
  21.147 -    | EXT Size DataRegister
  21.148 -    | ILLEGAL
  21.149 -    | JMP AddressingMode
  21.150 -    | JSR AddressingMode
  21.151 -    | LEA AddressingMode AddressRegister
  21.152 -    | LINK AddressRegister nat
  21.153 -    | LSL Size AddressingMode DataRegister
  21.154 -    | LSLW AddressingMode
  21.155 -    | LSR Size AddressingMode DataRegister
  21.156 -    | LSRW AddressingMode
  21.157 -    | MOVE Size AddressingMode AddressingMode
  21.158 -    | MOVEtoCCR AddressingMode
  21.159 -    | MOVEtoSR AddressingMode
  21.160 -    | MOVEfromSR AddressingMode
  21.161 -    | MOVEtoUSP AddressingMode
  21.162 -    | MOVEfromUSP AddressingMode
  21.163 -    | MOVEA Size AddressingMode AddressRegister
  21.164 -    | MOVEMto Size AddressingMode "DataOrAddressRegister list"
  21.165 -    | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
  21.166 -    | MOVEP Size AddressingMode AddressingMode
  21.167 -    | MOVEQ nat DataRegister
  21.168 -    | MULS AddressingMode DataRegister
  21.169 -    | MULU AddressingMode DataRegister
  21.170 -    | NBCD AddressingMode
  21.171 -    | NEG Size AddressingMode
  21.172 -    | NEGX Size AddressingMode
  21.173 -    | NOP
  21.174 -    | NOT Size AddressingMode
  21.175 -    | OR Size AddressingMode AddressingMode
  21.176 -    | ORI Size nat AddressingMode
  21.177 -    | ORItoCCR nat
  21.178 -    | ORItoSR nat
  21.179 -    | PEA AddressingMode
  21.180 -    | RESET
  21.181 -    | ROL Size AddressingMode DataRegister
  21.182 -    | ROLW AddressingMode
  21.183 -    | ROR Size AddressingMode DataRegister
  21.184 -    | RORW AddressingMode
  21.185 -    | ROXL Size AddressingMode DataRegister
  21.186 -    | ROXLW AddressingMode
  21.187 -    | ROXR Size AddressingMode DataRegister
  21.188 -    | ROXRW AddressingMode
  21.189 -    | RTE
  21.190 -    | RTR
  21.191 -    | RTS
  21.192 -    | SBCD AddressingMode AddressingMode
  21.193 -    | ST AddressingMode
  21.194 -    | SF AddressingMode
  21.195 -    | Scc Condition AddressingMode
  21.196 -    | STOP nat
  21.197 -    | SUB Size AddressingMode AddressingMode
  21.198 -    | SUBA Size AddressingMode AddressingMode
  21.199 -    | SUBI Size nat AddressingMode
  21.200 -    | SUBQ Size nat AddressingMode
  21.201 -    | SUBX Size AddressingMode AddressingMode
  21.202 -    | SWAP DataRegister
  21.203 -    | TAS AddressingMode
  21.204 -    | TRAP nat
  21.205 -    | TRAPV
  21.206 -    | TST Size AddressingMode
  21.207 -    | UNLK AddressRegister
  21.208 +old_datatype M68kInstruction =
  21.209 +  ABCD AddressingMode AddressingMode
  21.210 +| ADD Size AddressingMode AddressingMode
  21.211 +| ADDA Size AddressingMode AddressRegister
  21.212 +| ADDI Size nat AddressingMode
  21.213 +| ADDQ Size nat AddressingMode
  21.214 +| ADDX Size AddressingMode AddressingMode
  21.215 +| AND Size AddressingMode AddressingMode
  21.216 +| ANDI Size nat AddressingMode
  21.217 +| ANDItoCCR nat
  21.218 +| ANDItoSR nat
  21.219 +| ASL Size AddressingMode DataRegister
  21.220 +| ASLW AddressingMode
  21.221 +| ASR Size AddressingMode DataRegister
  21.222 +| ASRW AddressingMode
  21.223 +| Bcc Condition Size nat
  21.224 +| BTST Size AddressingMode AddressingMode
  21.225 +| BCHG Size AddressingMode AddressingMode
  21.226 +| BCLR Size AddressingMode AddressingMode
  21.227 +| BSET Size AddressingMode AddressingMode
  21.228 +| BRA Size nat
  21.229 +| BSR Size nat
  21.230 +| CHK AddressingMode DataRegister
  21.231 +| CLR Size AddressingMode
  21.232 +| CMP Size AddressingMode DataRegister
  21.233 +| CMPA Size AddressingMode AddressRegister
  21.234 +| CMPI Size nat AddressingMode
  21.235 +| CMPM Size AddressRegister AddressRegister
  21.236 +| DBT DataRegister nat
  21.237 +| DBF DataRegister nat
  21.238 +| DBcc Condition DataRegister nat
  21.239 +| DIVS AddressingMode DataRegister
  21.240 +| DIVU AddressingMode DataRegister
  21.241 +| EOR Size DataRegister AddressingMode
  21.242 +| EORI Size nat AddressingMode
  21.243 +| EORItoCCR nat
  21.244 +| EORItoSR nat
  21.245 +| EXG DataOrAddressRegister DataOrAddressRegister
  21.246 +| EXT Size DataRegister
  21.247 +| ILLEGAL
  21.248 +| JMP AddressingMode
  21.249 +| JSR AddressingMode
  21.250 +| LEA AddressingMode AddressRegister
  21.251 +| LINK AddressRegister nat
  21.252 +| LSL Size AddressingMode DataRegister
  21.253 +| LSLW AddressingMode
  21.254 +| LSR Size AddressingMode DataRegister
  21.255 +| LSRW AddressingMode
  21.256 +| MOVE Size AddressingMode AddressingMode
  21.257 +| MOVEtoCCR AddressingMode
  21.258 +| MOVEtoSR AddressingMode
  21.259 +| MOVEfromSR AddressingMode
  21.260 +| MOVEtoUSP AddressingMode
  21.261 +| MOVEfromUSP AddressingMode
  21.262 +| MOVEA Size AddressingMode AddressRegister
  21.263 +| MOVEMto Size AddressingMode "DataOrAddressRegister list"
  21.264 +| MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
  21.265 +| MOVEP Size AddressingMode AddressingMode
  21.266 +| MOVEQ nat DataRegister
  21.267 +| MULS AddressingMode DataRegister
  21.268 +| MULU AddressingMode DataRegister
  21.269 +| NBCD AddressingMode
  21.270 +| NEG Size AddressingMode
  21.271 +| NEGX Size AddressingMode
  21.272 +| NOP
  21.273 +| NOT Size AddressingMode
  21.274 +| OR Size AddressingMode AddressingMode
  21.275 +| ORI Size nat AddressingMode
  21.276 +| ORItoCCR nat
  21.277 +| ORItoSR nat
  21.278 +| PEA AddressingMode
  21.279 +| RESET
  21.280 +| ROL Size AddressingMode DataRegister
  21.281 +| ROLW AddressingMode
  21.282 +| ROR Size AddressingMode DataRegister
  21.283 +| RORW AddressingMode
  21.284 +| ROXL Size AddressingMode DataRegister
  21.285 +| ROXLW AddressingMode
  21.286 +| ROXR Size AddressingMode DataRegister
  21.287 +| ROXRW AddressingMode
  21.288 +| RTE
  21.289 +| RTR
  21.290 +| RTS
  21.291 +| SBCD AddressingMode AddressingMode
  21.292 +| ST AddressingMode
  21.293 +| SF AddressingMode
  21.294 +| Scc Condition AddressingMode
  21.295 +| STOP nat
  21.296 +| SUB Size AddressingMode AddressingMode
  21.297 +| SUBA Size AddressingMode AddressingMode
  21.298 +| SUBI Size nat AddressingMode
  21.299 +| SUBQ Size nat AddressingMode
  21.300 +| SUBX Size AddressingMode AddressingMode
  21.301 +| SWAP DataRegister
  21.302 +| TAS AddressingMode
  21.303 +| TRAP nat
  21.304 +| TRAPV
  21.305 +| TST Size AddressingMode
  21.306 +| UNLK AddressRegister
  21.307  
  21.308  end
    22.1 --- a/src/HOL/Fun_Def.thy	Thu Sep 11 18:54:36 2014 +0200
    22.2 +++ b/src/HOL/Fun_Def.thy	Thu Sep 11 18:54:36 2014 +0200
    22.3 @@ -97,7 +97,7 @@
    22.4  
    22.5  method_setup pat_completeness = {*
    22.6    Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
    22.7 -*} "prove completeness of datatype patterns"
    22.8 +*} "prove completeness of (co)datatype patterns"
    22.9  
   22.10  ML_file "Tools/Function/fun.ML"
   22.11  ML_file "Tools/Function/induction_schema.ML"
    23.1 --- a/src/HOL/HOLCF/FOCUS/Buffer.thy	Thu Sep 11 18:54:36 2014 +0200
    23.2 +++ b/src/HOL/HOLCF/FOCUS/Buffer.thy	Thu Sep 11 18:54:36 2014 +0200
    23.3 @@ -25,12 +25,10 @@
    23.4  
    23.5  typedecl D
    23.6  
    23.7 -datatype
    23.8 -
    23.9 +datatype_new
   23.10    M     = Md D | Mreq ("\<bullet>")
   23.11  
   23.12 -datatype
   23.13 -
   23.14 +datatype_new
   23.15    State = Sd D | Snil ("\<currency>")
   23.16  
   23.17  type_synonym
    24.1 --- a/src/HOL/Hoare/Hoare_Logic.thy	Thu Sep 11 18:54:36 2014 +0200
    24.2 +++ b/src/HOL/Hoare/Hoare_Logic.thy	Thu Sep 11 18:54:36 2014 +0200
    24.3 @@ -15,11 +15,11 @@
    24.4  type_synonym 'a bexp = "'a set"
    24.5  type_synonym 'a assn = "'a set"
    24.6  
    24.7 -datatype
    24.8 - 'a com = Basic "'a \<Rightarrow> 'a"
    24.9 -   | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
   24.10 -   | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
   24.11 -   | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
   24.12 +datatype_new 'a com =
   24.13 +  Basic "'a \<Rightarrow> 'a"
   24.14 +| Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
   24.15 +| Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
   24.16 +| While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
   24.17  
   24.18  abbreviation annskip ("SKIP") where "SKIP == Basic id"
   24.19  
    25.1 --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Thu Sep 11 18:54:36 2014 +0200
    25.2 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Thu Sep 11 18:54:36 2014 +0200
    25.3 @@ -12,12 +12,12 @@
    25.4  type_synonym 'a bexp = "'a set"
    25.5  type_synonym 'a assn = "'a set"
    25.6  
    25.7 -datatype
    25.8 - 'a com = Basic "'a \<Rightarrow> 'a"
    25.9 -   | Abort
   25.10 -   | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
   25.11 -   | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
   25.12 -   | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
   25.13 +datatype_new 'a com =
   25.14 +  Basic "'a \<Rightarrow> 'a"
   25.15 +| Abort
   25.16 +| Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
   25.17 +| Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
   25.18 +| While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
   25.19  
   25.20  abbreviation annskip ("SKIP") where "SKIP == Basic id"
   25.21  
    26.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Thu Sep 11 18:54:36 2014 +0200
    26.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Thu Sep 11 18:54:36 2014 +0200
    26.3 @@ -37,7 +37,7 @@
    26.4  and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
    26.5    n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
    26.6  
    26.7 -datatype 'a up = bot | Up 'a
    26.8 +old_datatype 'a up = bot | Up 'a
    26.9  
   26.10  instantiation up :: (SL_top)SL_top
   26.11  begin
    27.1 --- a/src/HOL/IMP/Com.thy	Thu Sep 11 18:54:36 2014 +0200
    27.2 +++ b/src/HOL/IMP/Com.thy	Thu Sep 11 18:54:36 2014 +0200
    27.3 @@ -2,7 +2,7 @@
    27.4  
    27.5  theory Com imports BExp begin
    27.6  
    27.7 -datatype
    27.8 +datatype_new
    27.9    com = SKIP 
   27.10        | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
   27.11        | Seq    com  com         ("_;;/ _"  [60, 61] 60)
    28.1 --- a/src/HOL/IMP/Procs.thy	Thu Sep 11 18:54:36 2014 +0200
    28.2 +++ b/src/HOL/IMP/Procs.thy	Thu Sep 11 18:54:36 2014 +0200
    28.3 @@ -6,7 +6,7 @@
    28.4  
    28.5  type_synonym pname = string
    28.6  
    28.7 -datatype
    28.8 +datatype_new
    28.9    com = SKIP 
   28.10        | Assign vname aexp        ("_ ::= _" [1000, 61] 61)
   28.11        | Seq    com  com          ("_;;/ _"  [60, 61] 60)
    29.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Thu Sep 11 18:54:36 2014 +0200
    29.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Thu Sep 11 18:54:36 2014 +0200
    29.3 @@ -53,11 +53,8 @@
    29.4  definition empty :: heap where
    29.5    "empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>"
    29.6  
    29.7 -datatype_new 'a array = Array addr -- "note the phantom type 'a"
    29.8 -datatype_compat array
    29.9 -
   29.10 -datatype_new 'a ref = Ref addr -- "note the phantom type 'a"
   29.11 -datatype_compat ref
   29.12 +old_datatype 'a array = Array addr -- "note the phantom type 'a"
   29.13 +old_datatype 'a ref = Ref addr -- "note the phantom type 'a"
   29.14  
   29.15  primrec addr_of_array :: "'a array \<Rightarrow> addr" where
   29.16    "addr_of_array (Array x) = x"
    30.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Sep 11 18:54:36 2014 +0200
    30.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Sep 11 18:54:36 2014 +0200
    30.3 @@ -11,7 +11,7 @@
    30.4  section {* Definition of Linked Lists *}
    30.5  
    30.6  setup {* Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>type ref"}) *}
    30.7 -datatype 'a node = Empty | Node 'a "'a node ref"
    30.8 +old_datatype 'a node = Empty | Node 'a "'a node ref"
    30.9  
   30.10  primrec
   30.11    node_encode :: "'a\<Colon>countable node \<Rightarrow> nat"
    31.1 --- a/src/HOL/Induct/Com.thy	Thu Sep 11 18:54:36 2014 +0200
    31.2 +++ b/src/HOL/Induct/Com.thy	Thu Sep 11 18:54:36 2014 +0200
    31.3 @@ -12,7 +12,7 @@
    31.4  typedecl loc
    31.5  type_synonym state = "loc => nat"
    31.6  
    31.7 -datatype
    31.8 +datatype_new
    31.9    exp = N nat
   31.10        | X loc
   31.11        | Op "nat => nat => nat" exp exp
    32.1 --- a/src/HOL/Induct/QuoDataType.thy	Thu Sep 11 18:54:36 2014 +0200
    32.2 +++ b/src/HOL/Induct/QuoDataType.thy	Thu Sep 11 18:54:36 2014 +0200
    32.3 @@ -10,7 +10,7 @@
    32.4  subsection{*Defining the Free Algebra*}
    32.5  
    32.6  text{*Messages with encryption and decryption as free constructors.*}
    32.7 -datatype
    32.8 +datatype_new
    32.9       freemsg = NONCE  nat
   32.10               | MPAIR  freemsg freemsg
   32.11               | CRYPT  nat freemsg  
    33.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Thu Sep 11 18:54:36 2014 +0200
    33.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Thu Sep 11 18:54:36 2014 +0200
    33.3 @@ -10,11 +10,13 @@
    33.4  subsection{*Defining the Free Algebra*}
    33.5  
    33.6  text{*Messages with encryption and decryption as free constructors.*}
    33.7 -datatype
    33.8 +datatype_new
    33.9       freeExp = VAR  nat
   33.10               | PLUS  freeExp freeExp
   33.11               | FNCALL  nat "freeExp list"
   33.12  
   33.13 +datatype_compat freeExp
   33.14 +
   33.15  text{*The equivalence relation, which makes PLUS associative.*}
   33.16  
   33.17  text{*The first rule is the desired equation. The next three rules
   33.18 @@ -38,7 +40,8 @@
   33.19  
   33.20  lemma exprel_refl: "X \<sim> X"
   33.21    and list_exprel_refl: "(Xs,Xs) \<in> listrel(exprel)"
   33.22 -  by (induct X and Xs) (blast intro: exprel.intros listrel.intros)+
   33.23 +  by (induct X and Xs rule: compat_freeExp.induct compat_freeExp_list.induct)
   33.24 +    (blast intro: exprel.intros listrel.intros)+
   33.25  
   33.26  theorem equiv_exprel: "equiv UNIV exprel"
   33.27  proof -
   33.28 @@ -306,7 +309,7 @@
   33.29  lemma vars_FnCall [simp]: "vars (FnCall F Xs) = vars_list Xs"
   33.30  apply (cases Xs rule: eq_Abs_ExpList) 
   33.31  apply (simp add: FnCall)
   33.32 -apply (induct_tac Us) 
   33.33 +apply (induct_tac Us)
   33.34  apply (simp_all add: vars_def UN_equiv_class [OF equiv_exprel vars_respects])
   33.35  done
   33.36  
   33.37 @@ -428,7 +431,7 @@
   33.38    obtain U where exp: "exp = (Abs_Exp (exprel `` {U}))" by (cases exp)
   33.39    obtain Us where list: "list = Abs_ExpList Us" by (rule eq_Abs_ExpList)
   33.40    have "P1 (Abs_Exp (exprel `` {U}))" and "P2 (Abs_ExpList Us)"
   33.41 -  proof (induct U and Us)
   33.42 +  proof (induct U and Us rule: compat_freeExp.induct compat_freeExp_list.induct)
   33.43      case (VAR nat)
   33.44      with V show ?case by (simp add: Var_def) 
   33.45    next
    34.1 --- a/src/HOL/Induct/SList.thy	Thu Sep 11 18:54:36 2014 +0200
    34.2 +++ b/src/HOL/Induct/SList.thy	Thu Sep 11 18:54:36 2014 +0200
    34.3 @@ -15,10 +15,10 @@
    34.4  
    34.5  so that list can serve as a "functor" for defining other recursive types.
    34.6  
    34.7 -This enables the conservative construction of mutual recursive data-types
    34.8 +This enables the conservative construction of mutual recursive datatypes
    34.9  such as
   34.10  
   34.11 -datatype 'a m = Node 'a * ('a m) list
   34.12 +datatype 'a m = Node 'a * 'a m list
   34.13  *)
   34.14  
   34.15  header {* Extended List Theory (old) *}
    35.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Thu Sep 11 18:54:36 2014 +0200
    35.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Thu Sep 11 18:54:36 2014 +0200
    35.3 @@ -30,7 +30,7 @@
    35.4    there are infinitely many elements in @{text "tyvrs"} and @{text "vrs"}. *}
    35.5  
    35.6  text{* The constructors for types and terms in System \FSUB{} contain abstractions 
    35.7 -  over type-variables and term-variables. The nominal datatype-package uses 
    35.8 +  over type-variables and term-variables. The nominal datatype package uses 
    35.9    @{text "\<guillemotleft>\<dots>\<guillemotright>\<dots>"} to indicate where abstractions occur. *}
   35.10  
   35.11  nominal_datatype ty = 
    36.1 --- a/src/HOL/Old_Datatype.thy	Thu Sep 11 18:54:36 2014 +0200
    36.2 +++ b/src/HOL/Old_Datatype.thy	Thu Sep 11 18:54:36 2014 +0200
    36.3 @@ -7,7 +7,7 @@
    36.4  
    36.5  theory Old_Datatype
    36.6  imports Power
    36.7 -keywords "datatype" :: thy_decl
    36.8 +keywords "old_datatype" :: thy_decl
    36.9  begin
   36.10  
   36.11  subsection {* The datatype universe *}
    37.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Thu Sep 11 18:54:36 2014 +0200
    37.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Thu Sep 11 18:54:36 2014 +0200
    37.3 @@ -10,7 +10,7 @@
    37.4  
    37.5  subsection{*Defining the Free Algebra*}
    37.6  
    37.7 -datatype
    37.8 +datatype_new
    37.9    freemsg = NONCE  nat
   37.10          | MPAIR  freemsg freemsg
   37.11          | CRYPT  nat freemsg
    38.1 --- a/src/HOL/SET_Protocol/Event_SET.thy	Thu Sep 11 18:54:36 2014 +0200
    38.2 +++ b/src/HOL/SET_Protocol/Event_SET.thy	Thu Sep 11 18:54:36 2014 +0200
    38.3 @@ -15,7 +15,7 @@
    38.4  
    38.5  
    38.6  text{*Message events*}
    38.7 -datatype
    38.8 +datatype_new
    38.9    event = Says  agent agent msg
   38.10          | Gets  agent       msg
   38.11          | Notes agent       msg
    39.1 --- a/src/HOL/SET_Protocol/Message_SET.thy	Thu Sep 11 18:54:36 2014 +0200
    39.2 +++ b/src/HOL/SET_Protocol/Message_SET.thy	Thu Sep 11 18:54:36 2014 +0200
    39.3 @@ -52,11 +52,11 @@
    39.4  
    39.5  text{*Agents. We allow any number of certification authorities, cardholders
    39.6              merchants, and payment gateways.*}
    39.7 -datatype
    39.8 +datatype_new
    39.9    agent = CA nat | Cardholder nat | Merchant nat | PG nat | Spy
   39.10  
   39.11  text{*Messages*}
   39.12 -datatype
   39.13 +datatype_new
   39.14       msg = Agent  agent     --{*Agent names*}
   39.15           | Number nat       --{*Ordinary integers, timestamps, ...*}
   39.16           | Nonce  nat       --{*Unguessable nonces*}
   39.17 @@ -373,6 +373,7 @@
   39.18  (*MPair case: blast_tac works out the necessary sum itself!*)
   39.19  prefer 2 apply (blast elim!: add_leE)
   39.20  (*Nonce case*)
   39.21 +apply (rename_tac nat)
   39.22  apply (rule_tac x = "N + Suc nat" in exI)
   39.23  apply (auto elim!: add_leE)
   39.24  done
   39.25 @@ -382,6 +383,7 @@
   39.26  apply (induct_tac "msg")
   39.27  apply (simp_all (no_asm_simp) add: exI parts_insert2)
   39.28  prefer 2 apply (blast elim!: add_leE)
   39.29 +apply (rename_tac nat)
   39.30  apply (rule_tac x = "N + Suc nat" in exI, auto)
   39.31  done
   39.32  
    40.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 11 18:54:36 2014 +0200
    40.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 11 18:54:36 2014 +0200
    40.3 @@ -1814,6 +1814,10 @@
    40.4    end;
    40.5  
    40.6  val _ =
    40.7 +  Outer_Syntax.local_theory @{command_spec "datatype"} "define inductive datatypes"
    40.8 +    (parse_co_datatype_cmd Least_FP construct_lfp);
    40.9 +
   40.10 +val _ =
   40.11    Outer_Syntax.local_theory @{command_spec "datatype_new"} "define inductive datatypes"
   40.12      (parse_co_datatype_cmd Least_FP construct_lfp);
   40.13  
    41.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Thu Sep 11 18:54:36 2014 +0200
    41.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Thu Sep 11 18:54:36 2014 +0200
    41.3 @@ -791,7 +791,7 @@
    41.4    >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
    41.5  
    41.6  val _ =
    41.7 -  Outer_Syntax.command @{command_spec "datatype"} "define old-style inductive datatypes"
    41.8 +  Outer_Syntax.command @{command_spec "old_datatype"} "define old-style inductive datatypes"
    41.9      (Parse.and_list1 spec_cmd
   41.10        >> (Toplevel.theory o (snd oo add_datatype_cmd Old_Datatype_Aux.default_config)));
   41.11  
    42.1 --- a/src/HOL/ex/Reflection_Examples.thy	Thu Sep 11 18:54:36 2014 +0200
    42.2 +++ b/src/HOL/ex/Reflection_Examples.thy	Thu Sep 11 18:54:36 2014 +0200
    42.3 @@ -17,7 +17,7 @@
    42.4  often need its structure.  Traditionnaly such simplifications are written in ML,
    42.5  proofs are synthesized.
    42.6  
    42.7 -An other strategy is to declare an HOL-datatype @{text \<tau>} and an HOL function (the
    42.8 +An other strategy is to declare an HOL datatype @{text \<tau>} and an HOL function (the
    42.9  interpretation) that maps elements of @{text \<tau>} to elements of @{text \<sigma>}.
   42.10  
   42.11  The functionality of @{text reify} then is, given a term @{text t} of type @{text \<sigma>},
    43.1 --- a/src/HOL/ex/Refute_Examples.thy	Thu Sep 11 18:54:36 2014 +0200
    43.2 +++ b/src/HOL/ex/Refute_Examples.thy	Thu Sep 11 18:54:36 2014 +0200
    43.3 @@ -507,10 +507,6 @@
    43.4  
    43.5  subsubsection {* Inductive datatypes *}
    43.6  
    43.7 -text {* With @{text quick_and_dirty} set, the datatype package does
    43.8 -  not generate certain axioms for recursion operators.  Without these
    43.9 -  axioms, Refute may find spurious countermodels. *}
   43.10 -
   43.11  text {* unit *}
   43.12  
   43.13  lemma "P (x::unit)"