--- a/NEWS Thu Sep 11 19:26:59 2014 +0200
+++ b/NEWS Thu Sep 11 19:32:36 2014 +0200
@@ -28,6 +28,9 @@
Minor INCOMPATIBILITY.
* New (co)datatype package:
+ - The 'datatype_new' command has been renamed 'datatype'. The old command of
+ that name is now called 'old_datatype'. See 'isabelle doc datatypes' for
+ information on porting.
- Renamed theorems:
disc_corec ~> corec_disc
disc_corec_iff ~> corec_disc_iff
@@ -58,6 +61,9 @@
INCOMPATIBILITY.
* Old datatype package:
+ - The old 'datatype' command has been renamed 'old_datatype', and
+ 'rep_datatype' has been renamed 'old_rep_datatype'. See
+ 'isabelle doc datatypes' for information on porting.
- Renamed theorems:
weak_case_cong ~> case_cong_weak
INCOMPATIBILITY.
--- a/src/Doc/Codegen/Evaluation.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/Doc/Codegen/Evaluation.thy Thu Sep 11 19:32:36 2014 +0200
@@ -205,7 +205,7 @@
An simplistic example:
*}
-datatype_new %quote form_ord = T | F | Less nat nat
+datatype %quote form_ord = T | F | Less nat nat
| And form_ord form_ord | Or form_ord form_ord | Neg form_ord
primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool"
@@ -259,7 +259,7 @@
example:
*}
-datatype_new %quote form = T | F | And form form | Or form form (*<*)
+datatype %quote form = T | F | And form form | Or form form (*<*)
(*>*) ML %quotett {*
fun eval_form @{code T} = true
--- a/src/Doc/Codegen/Introduction.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/Doc/Codegen/Introduction.thy Thu Sep 11 19:32:36 2014 +0200
@@ -35,7 +35,7 @@
subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *}
text {*
- In a HOL theory, the @{command_def datatype_new} and @{command_def
+ In a HOL theory, the @{command_def datatype} and @{command_def
definition}/@{command_def primrec}/@{command_def fun} declarations
form the core of a functional programming language. By default
equational theorems stemming from those are used for generated code,
@@ -45,7 +45,7 @@
For example, here a simple \qt{implementation} of amortised queues:
*}
-datatype_new %quote 'a queue = AQueue "'a list" "'a list"
+datatype %quote 'a queue = AQueue "'a list" "'a list"
definition %quote empty :: "'a queue" where
"empty = AQueue [] []"
--- a/src/Doc/Codegen/Refinement.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/Doc/Codegen/Refinement.thy Thu Sep 11 19:32:36 2014 +0200
@@ -87,7 +87,7 @@
queues:
*}
-datatype_new %quote 'a queue = Queue "'a list"
+datatype %quote 'a queue = Queue "'a list"
definition %quote empty :: "'a queue" where
"empty = Queue []"
--- a/src/Doc/Datatypes/Datatypes.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 11 19:32:36 2014 +0200
@@ -28,7 +28,7 @@
through a large class of non-datatypes, such as finite sets:
*}
- datatype_new 'a tree\<^sub>f\<^sub>s = Node\<^sub>f\<^sub>s (lbl\<^sub>f\<^sub>s: 'a) (sub\<^sub>f\<^sub>s: "'a tree\<^sub>f\<^sub>s fset")
+ datatype 'a tree\<^sub>f\<^sub>s = Node\<^sub>f\<^sub>s (lbl\<^sub>f\<^sub>s: 'a) (sub\<^sub>f\<^sub>s: "'a tree\<^sub>f\<^sub>s fset")
text {*
\noindent
@@ -37,7 +37,7 @@
context linorder
begin
- datatype_new flag = Less | Eq | Greater
+ datatype flag = Less | Eq | Greater
end
text {*
@@ -64,8 +64,8 @@
following four Rose tree examples:
*}
- datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
- datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
+ datatype (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
+ datatype (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f 'a "'a tree\<^sub>i\<^sub>f list"
codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
@@ -96,7 +96,7 @@
\setlength{\itemsep}{0pt}
\item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,''
-describes how to specify datatypes using the @{command datatype_new} command.
+describes how to specify datatypes using the @{command datatype} command.
\item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
Functions,'' describes how to specify recursive functions using
@@ -118,7 +118,7 @@
``Deriving Destructors and Theorems for Free Constructors,'' explains how to
use the command @{command free_constructors} to derive destructor constants
and theorems for freely generated types, as performed internally by @{command
-datatype_new} and @{command codatatype}.
+datatype} and @{command codatatype}.
%\item Section \ref{sec:using-the-standard-ml-interface}, ``Using the Standard
ML Interface,'' %describes the package's programmatic interface.
@@ -156,7 +156,7 @@
\label{sec:defining-datatypes} *}
text {*
-Datatypes can be specified using the @{command datatype_new} command.
+Datatypes can be specified using the @{command datatype} command.
*}
@@ -179,7 +179,7 @@
All their constructors are nullary:
*}
- datatype_new trool = Truue | Faalse | Perhaaps
+ datatype trool = Truue | Faalse | Perhaaps
text {*
\noindent
@@ -193,7 +193,7 @@
hide_const None Some map_option
hide_type option
(*>*)
- datatype_new 'a option = None | Some 'a
+ datatype 'a option = None | Some 'a
text {*
\noindent
@@ -203,7 +203,7 @@
The next example has three type parameters:
*}
- datatype_new ('a, 'b, 'c) triple = Triple 'a 'b 'c
+ datatype ('a, 'b, 'c) triple = Triple 'a 'b 'c
text {*
\noindent
@@ -213,7 +213,7 @@
is also possible:
*}
- datatype_new ('a, 'b, 'c) triple\<^sub>u = Triple\<^sub>u "'a * 'b * 'c"
+ datatype ('a, 'b, 'c) triple\<^sub>u = Triple\<^sub>u "'a * 'b * 'c"
text {*
\noindent
@@ -229,7 +229,7 @@
Natural numbers are the simplest example of a recursive type:
*}
- datatype_new nat = Zero | Succ nat
+ datatype nat = Zero | Succ nat
text {*
\noindent
@@ -237,7 +237,7 @@
stores a value of type @{typ 'b} at the very end:
*}
- datatype_new (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
+ datatype (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
subsubsection {* Mutual Recursion
@@ -249,7 +249,7 @@
natural numbers:
*}
- datatype_new even_nat = Even_Zero | Even_Succ odd_nat
+ datatype even_nat = Even_Zero | Even_Succ odd_nat
and odd_nat = Odd_Succ even_nat
text {*
@@ -258,7 +258,7 @@
expressions:
*}
- datatype_new ('a, 'b) exp =
+ datatype ('a, 'b) exp =
Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
and ('a, 'b) trm =
Factor "('a, 'b) fct" | Prod "('a, 'b) fct" "('a, 'b) trm"
@@ -276,7 +276,7 @@
follows:
*}
- datatype_new 'a btree =
+ datatype 'a btree =
BNode 'a "'a btree option" "'a btree option"
text {*
@@ -284,7 +284,7 @@
Not all nestings are admissible. For example, this command will fail:
*}
- datatype_new 'a wrong = W1 | W2 (*<*)'a
+ datatype 'a wrong = W1 | W2 (*<*)'a
typ (*>*)"'a wrong \<Rightarrow> 'a"
text {*
@@ -294,8 +294,8 @@
datatypes defined in terms of~@{text "\<Rightarrow>"}:
*}
- datatype_new ('a, 'b) fun_copy = Fun "'a \<Rightarrow> 'b"
- datatype_new 'a also_wrong = W1 | W2 (*<*)'a
+ datatype ('a, 'b) fun_copy = Fun "'a \<Rightarrow> 'b"
+ datatype 'a also_wrong = W1 | W2 (*<*)'a
typ (*>*)"('a also_wrong, 'a) fun_copy"
text {*
@@ -303,14 +303,14 @@
The following definition of @{typ 'a}-branching trees is legal:
*}
- datatype_new 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
+ datatype 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
text {*
\noindent
And so is the definition of hereditarily finite sets:
*}
- datatype_new hfset = HFSet "hfset fset"
+ datatype hfset = HFSet "hfset fset"
text {*
\noindent
@@ -323,15 +323,15 @@
Type constructors must be registered as BNFs to have live arguments. This is
done automatically for datatypes and codatatypes introduced by the @{command
-datatype_new} and @{command codatatype} commands.
+datatype} and @{command codatatype} commands.
Section~\ref{sec:introducing-bounded-natural-functors} explains how to
register arbitrary type constructors as BNFs.
Here is another example that fails:
*}
- datatype_new 'a pow_list = PNil 'a (*<*)'a
- datatype_new 'a pow_list' = PNil' 'a (*>*)| PCons "('a * 'a) pow_list"
+ datatype 'a pow_list = PNil 'a (*<*)'a
+ datatype 'a pow_list' = PNil' 'a (*>*)| PCons "('a * 'a) pow_list"
text {*
\noindent
@@ -345,7 +345,7 @@
\label{sssec:datatype-auxiliary-constants-and-properties} *}
text {*
-The @{command datatype_new} command introduces various constants in addition to
+The @{command datatype} command introduces various constants in addition to
the constructors. With each datatype are associated set functions, a map
function, a relator, discriminators, and selectors, all of which can be given
custom names. In the example below, the familiar names @{text null}, @{text hd},
@@ -368,7 +368,7 @@
context early begin
(*>*)
- datatype_new (set: 'a) list =
+ datatype (set: 'a) list =
null: Nil
| Cons (hd: 'a) (tl: "'a list")
for
@@ -433,11 +433,11 @@
(*<*)
end
(*>*)
- datatype_new ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
+ datatype ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
text {* \blankline *}
- datatype_new (set: 'a) list =
+ datatype (set: 'a) list =
null: Nil ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
for
@@ -461,16 +461,16 @@
subsection {* Command Syntax
\label{ssec:datatype-command-syntax} *}
-subsubsection {* \keyw{datatype_new}
+subsubsection {* \keyw{datatype}
\label{sssec:datatype-new} *}
text {*
\begin{matharray}{rcl}
- @{command_def "datatype_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
+ @{command_def "datatype"} & : & @{text "local_theory \<rightarrow> local_theory"}
\end{matharray}
@{rail \<open>
- @@{command datatype_new} target? @{syntax dt_options}? \<newline>
+ @@{command datatype} target? @{syntax dt_options}? \<newline>
(@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \<newline>
@{syntax map_rel}? (@'where' (prop + '|'))? + @'and')
;
@@ -484,7 +484,7 @@
\medskip
\noindent
-The @{command datatype_new} command introduces a set of mutually recursive
+The @{command datatype} command introduces a set of mutually recursive
datatypes specified by their constructors.
The syntactic entity \synt{target} can be used to specify a local
@@ -667,7 +667,7 @@
\label{ssec:datatype-generated-theorems} *}
text {*
-The characteristic theorems generated by @{command datatype_new} are grouped in
+The characteristic theorems generated by @{command datatype} are grouped in
three broad categories:
\begin{itemize}
@@ -1009,7 +1009,7 @@
\end{indentblock}
\noindent
-For convenience, @{command datatype_new} also provides the following collection:
+For convenience, @{command datatype} also provides the following collection:
\begin{indentblock}
\begin{description}
@@ -1026,7 +1026,7 @@
\label{ssec:datatype-compatibility-issues} *}
text {*
-The command @{command datatype_new} has been designed to be highly compatible
+The command @{command datatype} has been designed to be highly compatible
with the old command (which is now called \keyw{old_datatype}), to ease
migration. There are nonetheless a few incompatibilities that may arise when
porting:
@@ -1268,7 +1268,7 @@
*}
(*<*)
- datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f (lbl\<^sub>f\<^sub>f: 'a) (sub\<^sub>f\<^sub>f: "'a tree\<^sub>f\<^sub>f list")
+ datatype 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f (lbl\<^sub>f\<^sub>f: 'a) (sub\<^sub>f\<^sub>f: "'a tree\<^sub>f\<^sub>f list")
(*>*)
primrec at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
"at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
@@ -1322,7 +1322,7 @@
$n = 2$:
*}
- datatype_new 'a ftree2 = FTLeaf2 'a | FTNode2 "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2"
+ datatype 'a ftree2 = FTLeaf2 'a | FTNode2 "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2"
text {* \blankline *}
@@ -1533,7 +1533,7 @@
text {* \blankline *}
- datatype_new ('a, 'b) tlist =
+ datatype ('a, 'b) tlist =
TNil (termi: 'b)
| TCons (thd: 'a) (ttl: "('a, 'b) tlist")
where
@@ -2455,7 +2455,7 @@
lazy lists. The cardinal bound limits the number of elements returned by the
set function; it may not depend on the cardinality of @{typ 'a}.
-The type constructors introduced by @{command datatype_new} and
+The type constructors introduced by @{command datatype} and
@{command codatatype} are automatically registered as BNFs. In addition, a
number of old-style datatypes and non-free types are preregistered.
@@ -2653,7 +2653,7 @@
@{text dead} in front of the type variable (e.g., @{text "(dead 'a)"})
instead of an identifier for the corresponding set function. Witnesses can be
specified by their types. Otherwise, the syntax of @{command bnf_axiomatization}
-is identical to the left-hand side of a @{command datatype_new} or
+is identical to the left-hand side of a @{command datatype} or
@{command codatatype} definition.
The command is useful to reason abstractly about BNFs. The axioms are safe
@@ -2682,7 +2682,7 @@
text {*
The derivation of convenience theorems for types equipped with free constructors,
-as performed internally by @{command datatype_new} and @{command codatatype},
+as performed internally by @{command datatype} and @{command codatatype},
is available as a stand-alone command called @{command free_constructors}.
% * need for this is rare but may arise if you want e.g. to add destructors to
@@ -2731,7 +2731,7 @@
\synt{name} denotes an identifier, \synt{prop} denotes a HOL proposition, and
\synt{term} denotes a HOL term \cite{isabelle-isar-ref}.
-The syntax resembles that of @{command datatype_new} and @{command codatatype}
+The syntax resembles that of @{command datatype} and @{command codatatype}
definitions (Sections
\ref{ssec:datatype-command-syntax}~and~\ref{ssec:codatatype-command-syntax}).
A constructor is specified by an optional name for the discriminator, the
@@ -2761,13 +2761,13 @@
Plugins extend the (co)datatype package to interoperate with other Isabelle
packages and tools, such as the code generator, Transfer, Lifting, and
Quickcheck. They can be enabled or disabled individually using the
-@{syntax plugins} option to the commands @{command datatype_new},
+@{syntax plugins} option to the commands @{command datatype},
@{command codatatype}, @{command free_constructors}, @{command bnf}, and
@{command bnf_axiomatization}.
For example:
*}
- datatype_new (plugins del: code "quickcheck_*") color = Red | Black
+ datatype (plugins del: code "quickcheck_*") color = Red | Black
subsection {* Code Generator
--- a/src/Doc/Datatypes/document/root.tex Thu Sep 11 19:26:59 2014 +0200
+++ b/src/Doc/Datatypes/document/root.tex Thu Sep 11 19:32:36 2014 +0200
@@ -77,7 +77,7 @@
\begin{abstract}
\noindent
This tutorial describes the definitional package for datatypes and codatatypes
-in Isabelle/HOL. The package provides four main commands: \keyw{datatype_new},
+in Isabelle/HOL. The package provides four main commands: \keyw{datatype},
\keyw{codatatype}, \keyw{primrec}, and \keyw{primcorec}.
\end{abstract}
--- a/src/Doc/Functions/Functions.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/Doc/Functions/Functions.thy Thu Sep 11 19:32:36 2014 +0200
@@ -522,7 +522,7 @@
and @{term "X"} for true, false and uncertain propositions, respectively.
*}
-datatype_new P3 = T | F | X
+datatype P3 = T | F | X
text {* \noindent Then the conjunction of such values can be defined as follows: *}
@@ -1122,7 +1122,7 @@
As an example, imagine a datatype of n-ary trees:
*}
-datatype_new 'a tree =
+datatype 'a tree =
Leaf 'a
| Branch "'a tree list"
--- a/src/Doc/Isar_Ref/Generic.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Thu Sep 11 19:32:36 2014 +0200
@@ -736,7 +736,7 @@
monotonically through the theory hierarchy: forming a new theory,
the union of the simpsets of its imports are taken as starting
point. Also note that definitional packages like @{command
- "datatype_new"}, @{command "primrec"}, @{command "fun"} routinely
+ "datatype"}, @{command "primrec"}, @{command "fun"} routinely
declare Simplifier rules to the target context, while plain
@{command "definition"} is an exception in \emph{not} declaring
anything.
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Sep 11 19:32:36 2014 +0200
@@ -283,7 +283,7 @@
\begin{description}
\item @{command (HOL) "primrec"} defines primitive recursive
- functions over datatypes (see also @{command_ref (HOL) datatype_new}).
+ functions over datatypes (see also @{command_ref (HOL) datatype}).
The given @{text equations} specify reduction rules that are produced
by instantiating the generic combinator for primitive recursion that
is available for each datatype.
@@ -378,7 +378,7 @@
boolean expressions, and use @{command primrec} for evaluation
functions that follow the same recursive structure. *}
-datatype_new 'a aexp =
+datatype 'a aexp =
IF "'a bexp" "'a aexp" "'a aexp"
| Sum "'a aexp" "'a aexp"
| Diff "'a aexp" "'a aexp"
@@ -449,7 +449,7 @@
text {* Functions on datatypes with nested recursion are also defined
by mutual primitive recursion. *}
-datatype_new ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
+datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
text {* A substitution function on type @{typ "('a, 'b) term"} can be
defined as follows, by working simultaneously on @{typ "('a, 'b)
@@ -479,7 +479,7 @@
primitive recursion is just as easy.
*}
-datatype_new 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
+datatype 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
where
@@ -749,7 +749,7 @@
names than the existing @{typ "'a list"} that is already in @{theory
Main}: *}
-datatype_new 'a seq = Empty | Seq 'a "'a seq"
+datatype 'a seq = Empty | Seq 'a "'a seq"
text {* We can now prove some simple lemma by structural induction: *}
@@ -1158,9 +1158,9 @@
by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject)
text {* Note that such trivial constructions are better done with
- derived specification mechanisms such as @{command datatype_new}: *}
-
-datatype_new three' = One' | Two' | Three'
+ derived specification mechanisms such as @{command datatype}: *}
+
+datatype three' = One' | Two' | Three'
text {* This avoids re-doing basic definitions and proofs from the
primitive @{command typedef} above. *}
@@ -2354,7 +2354,7 @@
to reason about inductive types. Rules are selected according to
the declarations by the @{attribute cases} and @{attribute induct}
attributes, cf.\ \secref{sec:cases-induct}. The @{command (HOL)
- datatype_new} package already takes care of this.
+ datatype} package already takes care of this.
These unstructured tactics feature both goal addressing and dynamic
instantiation. Note that named rule cases are \emph{not} provided
--- a/src/Doc/Isar_Ref/Synopsis.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/Doc/Isar_Ref/Synopsis.thy Thu Sep 11 19:32:36 2014 +0200
@@ -1068,7 +1068,7 @@
provide suitable derived cases rules.
*}
-datatype_new foo = Foo | Bar foo
+datatype foo = Foo | Bar foo
notepad
begin
--- a/src/HOL/Auth/Event.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Auth/Event.thy Thu Sep 11 19:32:36 2014 +0200
@@ -15,7 +15,7 @@
consts (*Initial states of agents -- parameter of the construction*)
initState :: "agent => msg set"
-datatype_new
+datatype
event = Says agent agent msg
| Gets agent msg
| Notes agent msg
--- a/src/HOL/Auth/Message.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Auth/Message.thy Thu Sep 11 19:32:36 2014 +0200
@@ -35,10 +35,10 @@
definition symKeys :: "key set" where
"symKeys == {K. invKey K = K}"
-datatype_new --{*We allow any number of friendly agents*}
+datatype --{*We allow any number of friendly agents*}
agent = Server | Friend nat | Spy
-datatype_new
+datatype
msg = Agent agent --{*Agent names*}
| Number nat --{*Ordinary integers, timestamps, ...*}
| Nonce nat --{*Unguessable nonces*}
--- a/src/HOL/Auth/Public.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Auth/Public.thy Thu Sep 11 19:32:36 2014 +0200
@@ -16,7 +16,7 @@
subsection{*Asymmetric Keys*}
-datatype_new keymode = Signature | Encryption
+datatype keymode = Signature | Encryption
consts
publicKey :: "[keymode,agent] => key"
--- a/src/HOL/Auth/Smartcard/EventSC.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Auth/Smartcard/EventSC.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,10 +9,10 @@
consts (*Initial states of agents -- parameter of the construction*)
initState :: "agent => msg set"
-datatype_new card = Card agent
+datatype card = Card agent
text{*Four new events express the traffic between an agent and his card*}
-datatype_new
+datatype
event = Says agent agent msg
| Notes agent msg
| Gets agent msg
--- a/src/HOL/Auth/TLS.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Auth/TLS.thy Thu Sep 11 19:32:36 2014 +0200
@@ -49,7 +49,7 @@
signature. Therefore, we formalize signature as encryption using the
private encryption key.*}
-datatype_new role = ClientRole | ServerRole
+datatype role = ClientRole | ServerRole
consts
(*Pseudo-random function of Section 5*)
--- a/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 11 19:32:36 2014 +0200
@@ -13,7 +13,7 @@
imports BNF_Fixpoint_Base
keywords
"datatype" :: thy_decl and
- "datatype_new" :: thy_decl and
+ "datatype" :: thy_decl and
"datatype_compat" :: thy_decl
begin
--- a/src/HOL/Bali/AxSem.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Bali/AxSem.thy Thu Sep 11 19:32:36 2014 +0200
@@ -378,7 +378,7 @@
\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
\<and> s\<Colon>\<preceq>(G,L))"
-datatype_new 'a triple = triple "('a assn)" "term" "('a assn)" (** should be
+datatype 'a triple = triple "('a assn)" "term" "('a assn)" (** should be
something like triple = \<forall>'a. triple ('a assn) term ('a assn) **)
("{(1_)}/ _>/ {(1_)}" [3,65,3]75)
type_synonym 'a triples = "'a triple set"
--- a/src/HOL/Bali/Basis.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Bali/Basis.thy Thu Sep 11 19:32:36 2014 +0200
@@ -155,7 +155,7 @@
primrec the_Inr :: "'a + 'b \<Rightarrow> 'b"
where "the_Inr (Inr b) = b"
-datatype_new ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
+datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
primrec the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
where "the_In1 (In1 a) = a"
--- a/src/HOL/Bali/Decl.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Bali/Decl.thy Thu Sep 11 19:32:36 2014 +0200
@@ -42,7 +42,7 @@
subsubsection {* Access modifier *}
-datatype_new acc_modi (* access modifier *)
+datatype acc_modi (* access modifier *)
= Private | Package | Protected | Public
text {*
@@ -223,9 +223,9 @@
introduce the notion of a member declaration (e.g. useful to define
accessiblity ) *}
-datatype_new memberdecl = fdecl fdecl | mdecl mdecl
+datatype memberdecl = fdecl fdecl | mdecl mdecl
-datatype_new memberid = fid vname | mid sig
+datatype memberid = fid vname | mid sig
class has_memberid =
fixes memberid :: "'a \<Rightarrow> memberid"
--- a/src/HOL/Bali/Example.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Bali/Example.thy Thu Sep 11 19:32:36 2014 +0200
@@ -66,9 +66,9 @@
section "type and expression names"
(** unfortunately cannot simply instantiate tnam **)
-datatype_new tnam' = HasFoo' | Base' | Ext' | Main'
-datatype_new vnam' = arr' | vee' | z' | e'
-datatype_new label' = lab1'
+datatype tnam' = HasFoo' | Base' | Ext' | Main'
+datatype vnam' = arr' | vee' | z' | e'
+datatype label' = lab1'
axiomatization
tnam' :: "tnam' \<Rightarrow> tnam" and
--- a/src/HOL/Bali/Name.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Bali/Name.thy Thu Sep 11 19:32:36 2014 +0200
@@ -12,11 +12,11 @@
typedecl vname --{* variable or field name *}
typedecl label --{* label as destination of break or continue *}
-datatype_new ename --{* expression name *}
+datatype ename --{* expression name *}
= VNam vname
| Res --{* special name to model the return value of methods *}
-datatype_new lname --{* names for local variables and the This pointer *}
+datatype lname --{* names for local variables and the This pointer *}
= EName ename
| This
abbreviation VName :: "vname \<Rightarrow> lname"
@@ -25,7 +25,7 @@
abbreviation Result :: lname
where "Result == EName Res"
-datatype_new xname --{* names of standard exceptions *}
+datatype xname --{* names of standard exceptions *}
= Throwable
| NullPointer | OutOfMemory | ClassCast
| NegArrSize | IndOutBound | ArrStore
@@ -39,7 +39,7 @@
done
-datatype_new tname --{* type names for standard classes and other type names *}
+datatype tname --{* type names for standard classes and other type names *}
= Object'
| SXcpt' xname
| TName tnam
--- a/src/HOL/Bali/State.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Bali/State.thy Thu Sep 11 19:32:36 2014 +0200
@@ -19,7 +19,7 @@
section "objects"
-datatype_new obj_tag = --{* tag for generic object *}
+datatype obj_tag = --{* tag for generic object *}
CInst qtname --{* class instance *}
| Arr ty int --{* array with component type and length *}
--{* | CStat qtname the tag is irrelevant for a class object,
@@ -225,7 +225,7 @@
(type) "heap" <= (type) "(loc , obj) table"
(* (type) "locals" <= (type) "(lname, val) table" *)
-datatype_new st = (* pure state, i.e. contents of all variables *)
+datatype st = (* pure state, i.e. contents of all variables *)
st globs locals
subsection "access"
--- a/src/HOL/Bali/Term.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Bali/Term.thy Thu Sep 11 19:32:36 2014 +0200
@@ -60,20 +60,20 @@
type_synonym locals = "(lname, val) table" --{* local variables *}
-datatype_new jump
+datatype jump
= Break label --{* break *}
| Cont label --{* continue *}
| Ret --{* return from method *}
-datatype_new xcpt --{* exception *}
+datatype xcpt --{* exception *}
= Loc loc --{* location of allocated execption object *}
| Std xname --{* intermediate standard exception, see Eval.thy *}
-datatype_new error
+datatype error
= AccessViolation --{* Access to a member that isn't permitted *}
| CrossMethodJump --{* Method exits with a break or continue *}
-datatype_new abrupt --{* abrupt completion *}
+datatype abrupt --{* abrupt completion *}
= Xcpt xcpt --{* exception *}
| Jump jump --{* break, continue, return *}
| Error error -- {* runtime errors, we wan't to detect and proof absent
@@ -90,7 +90,7 @@
translations
(type) "locals" <= (type) "(lname, val) table"
-datatype_new inv_mode --{* invocation mode for method calls *}
+datatype inv_mode --{* invocation mode for method calls *}
= Static --{* static *}
| SuperM --{* super *}
| IntVir --{* interface or virtual *}
@@ -104,13 +104,13 @@
(type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
--{* function codes for unary operations *}
-datatype_new unop = UPlus -- {*{\tt +} unary plus*}
+datatype unop = UPlus -- {*{\tt +} unary plus*}
| UMinus -- {*{\tt -} unary minus*}
| UBitNot -- {*{\tt ~} bitwise NOT*}
| UNot -- {*{\tt !} logical complement*}
--{* function codes for binary operations *}
-datatype_new binop = Mul -- {*{\tt * } multiplication*}
+datatype binop = Mul -- {*{\tt * } multiplication*}
| Div -- {*{\tt /} division*}
| Mod -- {*{\tt \%} remainder*}
| Plus -- {*{\tt +} addition*}
@@ -140,7 +140,7 @@
{\tt true || e} e is not evaluated;
*}
-datatype_new var
+datatype var
= LVar lname --{* local variable (incl. parameters) *}
| FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90)
--{* class field *}
--- a/src/HOL/Bali/Type.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Bali/Type.thy Thu Sep 11 19:32:36 2014 +0200
@@ -14,13 +14,13 @@
\end{itemize}
*}
-datatype_new prim_ty --{* primitive type, cf. 4.2 *}
+datatype prim_ty --{* primitive type, cf. 4.2 *}
= Void --{* result type of void methods *}
| Boolean
| Integer
-datatype_new ref_ty --{* reference type, cf. 4.3 *}
+datatype ref_ty --{* reference type, cf. 4.3 *}
= NullT --{* null type, cf. 4.1 *}
| IfaceT qtname --{* interface type *}
| ClassT qtname --{* class type *}
--- a/src/HOL/Bali/Value.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Bali/Value.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
typedecl loc --{* locations, i.e. abstract references on objects *}
-datatype_new val
+datatype val
= Unit --{* dummy result value of void methods *}
| Bool bool --{* Boolean value *}
| Intg int --{* integer value *}
--- a/src/HOL/Code_Evaluation.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Code_Evaluation.thy Thu Sep 11 19:32:36 2014 +0200
@@ -13,7 +13,7 @@
subsubsection {* Terms and class @{text term_of} *}
-datatype_new "term" = dummy_term
+datatype "term" = dummy_term
definition Const :: "String.literal \<Rightarrow> typerep \<Rightarrow> term" where
"Const _ _ = dummy_term"
--- a/src/HOL/Codegenerator_Test/Code_Test.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test.thy Thu Sep 11 19:32:36 2014 +0200
@@ -11,7 +11,7 @@
subsection {* YXML encoding for @{typ Code_Evaluation.term} *}
-datatype_new yxml_of_term = YXML
+datatype yxml_of_term = YXML
lemma yot_anything: "x = (y :: yxml_of_term)"
by(cases x y rule: yxml_of_term.exhaust[case_product yxml_of_term.exhaust])(simp)
@@ -58,7 +58,7 @@
sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}.
*}
-datatype_new xml_tree = XML_Tree
+datatype xml_tree = XML_Tree
lemma xml_tree_anything: "x = (y :: xml_tree)"
by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)
--- a/src/HOL/Datatype_Examples/Compat.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Datatype_Examples/Compat.thy Thu Sep 11 19:32:36 2014 +0200
@@ -31,7 +31,7 @@
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name old_lst}; \<close>
-datatype_new 'a lst = Nl | Cns 'a "'a lst"
+datatype 'a lst = Nl | Cns 'a "'a lst"
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name lst}; \<close>
@@ -39,7 +39,7 @@
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name lst}; \<close>
-datatype_new 'b w = W | W' "'b w \<times> 'b list"
+datatype 'b w = W | W' "'b w \<times> 'b list"
(* no support for sums of products:
datatype_compat w
@@ -47,11 +47,11 @@
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name w}; \<close>
-datatype_new ('c, 'b) s = L 'c | R 'b
+datatype ('c, 'b) s = L 'c | R 'b
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name s}; \<close>
-datatype_new 'd x = X | X' "('d x lst, 'd list) s"
+datatype 'd x = X | X' "('d x lst, 'd list) s"
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name x}; \<close>
@@ -67,7 +67,7 @@
thm x.induct x.rec
thm compat_x.induct compat_x.rec
-datatype_new 'a tttre = TTTre 'a "'a tttre lst lst lst"
+datatype 'a tttre = TTTre 'a "'a tttre lst lst lst"
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tttre}; \<close>
@@ -78,7 +78,7 @@
thm tttre.induct tttre.rec
thm compat_tttre.induct compat_tttre.rec
-datatype_new 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst"
+datatype 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst"
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name ftre}; \<close>
@@ -89,7 +89,7 @@
thm ftre.induct ftre.rec
thm compat_ftre.induct compat_ftre.rec
-datatype_new 'a btre = BTre 'a "'a btre lst" "'a btre lst"
+datatype 'a btre = BTre 'a "'a btre lst" "'a btre lst"
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name btre}; \<close>
@@ -100,7 +100,7 @@
thm btre.induct btre.rec
thm compat_btre.induct compat_btre.rec
-datatype_new 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo"
+datatype 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo"
ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo}; \<close>
ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar}; \<close>
@@ -110,7 +110,7 @@
ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo}; \<close>
ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar}; \<close>
-datatype_new 'a tre = Tre 'a "'a tre lst"
+datatype 'a tre = Tre 'a "'a tre lst"
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tre}; \<close>
@@ -121,12 +121,12 @@
thm tre.induct tre.rec
thm compat_tre.induct compat_tre.rec
-datatype_new 'a f = F 'a and 'a g = G 'a
+datatype 'a f = F 'a and 'a g = G 'a
ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name f}; \<close>
ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name g}; \<close>
-datatype_new h = H "h f" | H'
+datatype h = H "h f" | H'
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name h}; \<close>
@@ -143,7 +143,7 @@
thm h.induct h.rec
thm compat_h.induct compat_h.rec
-datatype_new myunit = MyUnity
+datatype myunit = MyUnity
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name myunit}; \<close>
@@ -151,7 +151,7 @@
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name myunit}; \<close>
-datatype_new mylist = MyNil | MyCons nat mylist
+datatype mylist = MyNil | MyCons nat mylist
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name mylist}; \<close>
@@ -159,7 +159,7 @@
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name mylist}; \<close>
-datatype_new foo' = FooNil | FooCons bar' foo' and bar' = Bar
+datatype foo' = FooNil | FooCons bar' foo' and bar' = Bar
ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo'}; \<close>
ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar'}; \<close>
@@ -177,7 +177,7 @@
ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name fnky}; \<close>
-datatype_new tree = Tree "tree foo"
+datatype tree = Tree "tree foo"
ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tree}; \<close>
--- a/src/HOL/Datatype_Examples/IsaFoR_Datatypes.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Datatype_Examples/IsaFoR_Datatypes.thy Thu Sep 11 19:32:36 2014 +0200
@@ -11,16 +11,16 @@
imports Real
begin
-datatype_new (discs_sels) ('f, 'l) lab =
+datatype (discs_sels) ('f, 'l) lab =
Lab "('f, 'l) lab" 'l
| FunLab "('f, 'l) lab" "('f, 'l) lab list"
| UnLab 'f
| Sharp "('f, 'l) lab"
-datatype_new (discs_sels) 'f projL = Projection "(('f \<times> nat) \<times> nat) list"
+datatype (discs_sels) 'f projL = Projection "(('f \<times> nat) \<times> nat) list"
-datatype_new (discs_sels) ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
-datatype_new (discs_sels) ('f, 'v) ctxt =
+datatype (discs_sels) ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
+datatype (discs_sels) ('f, 'v) ctxt =
Hole ("\<box>")
| More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list"
@@ -32,7 +32,7 @@
type_synonym ('f, 'l, 'v) trsLL = "(('f, 'l) lab, 'v) rules"
type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list"
-datatype_new (discs_sels) pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70)
+datatype (discs_sels) pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70)
type_synonym ('f, 'v) prseq = "(pos \<times> ('f, 'v) rule \<times> bool \<times> ('f, 'v) term) list"
type_synonym ('f, 'v) rseq = "(pos \<times> ('f, 'v) rule \<times> ('f, 'v) term) list"
@@ -49,7 +49,7 @@
type_synonym ('f, 'l, 'v) qtrsLL =
"bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL"
-datatype_new (discs_sels) location = H | A | B | R
+datatype (discs_sels) location = H | A | B | R
type_synonym ('f, 'v) forb_pattern = "('f, 'v) ctxt \<times> ('f, 'v) term \<times> location"
type_synonym ('f, 'v) forb_patterns = "('f, 'v) forb_pattern set"
@@ -68,20 +68,20 @@
type_synonym 'a vec = "'a list"
type_synonym 'a mat = "'a vec list"
-datatype_new (discs_sels) arctic = MinInfty | Num_arc int
-datatype_new (discs_sels) 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
-datatype_new (discs_sels) order_tag = Lex | Mul
+datatype (discs_sels) arctic = MinInfty | Num_arc int
+datatype (discs_sels) 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
+datatype (discs_sels) order_tag = Lex | Mul
type_synonym 'f status_prec_repr = "(('f \<times> nat) \<times> (nat \<times> order_tag)) list"
-datatype_new (discs_sels) af_entry =
+datatype (discs_sels) af_entry =
Collapse nat
| AFList "nat list"
type_synonym 'f afs_list = "(('f \<times> nat) \<times> af_entry) list"
type_synonym 'f prec_weight_repr = "(('f \<times> nat) \<times> (nat \<times> nat \<times> (nat list option))) list \<times> nat"
-datatype_new (discs_sels) 'f redtriple_impl =
+datatype (discs_sels) 'f redtriple_impl =
Int_carrier "('f, int) lpoly_interL"
| Int_nl_carrier "('f, int) poly_inter_list"
| Rat_carrier "('f, rat) lpoly_interL"
@@ -98,15 +98,15 @@
| RPO "'f status_prec_repr" "'f afs_list"
| KBO "'f prec_weight_repr" "'f afs_list"
-datatype_new (discs_sels) list_order_type = MS_Ext | Max_Ext | Min_Ext | Dms_Ext
+datatype (discs_sels) list_order_type = MS_Ext | Max_Ext | Min_Ext | Dms_Ext
type_synonym 'f scnp_af = "(('f \<times> nat) \<times> (nat \<times> nat) list) list"
-datatype_new (discs_sels) 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"
+datatype (discs_sels) 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"
type_synonym 'f sig_map_list = "(('f \<times> nat) \<times> 'f list) list"
type_synonym ('f, 'v) uncurry_info = "'f \<times> 'f sig_map_list \<times> ('f, 'v) rules \<times> ('f, 'v) rules"
-datatype_new (discs_sels) arithFun =
+datatype (discs_sels) arithFun =
Arg nat
| Const nat
| Sum "arithFun list"
@@ -115,25 +115,25 @@
| Prod "arithFun list"
| IfEqual arithFun arithFun arithFun arithFun
-datatype_new (discs_sels) 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list"
-datatype_new (discs_sels) ('f, 'v) sl_variant =
+datatype (discs_sels) 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list"
+datatype (discs_sels) ('f, 'v) sl_variant =
Rootlab "('f \<times> nat) option"
| Finitelab "'f sl_inter"
| QuasiFinitelab "'f sl_inter" 'v
type_synonym ('f, 'v) crit_pair_joins = "(('f, 'v) term \<times> ('f, 'v) rseq \<times> ('f, 'v) term \<times> ('f, 'v) rseq) list"
-datatype_new (discs_sels) 'f join_info = Guided "('f, string) crit_pair_joins" | Join_NF | Join_BFS nat
+datatype (discs_sels) 'f join_info = Guided "('f, string) crit_pair_joins" | Join_NF | Join_BFS nat
type_synonym unknown_info = string
type_synonym dummy_prf = unit
-datatype_new (discs_sels) ('f, 'v) complex_constant_removal_prf = Complex_Constant_Removal_Proof
+datatype (discs_sels) ('f, 'v) complex_constant_removal_prf = Complex_Constant_Removal_Proof
"('f, 'v) term"
"(('f, 'v) rule \<times> ('f, 'v) rule) list"
-datatype_new (discs_sels) ('f, 'v) cond_constraint =
+datatype (discs_sels) ('f, 'v) cond_constraint =
CC_cond bool "('f, 'v) rule"
| CC_rewr "('f, 'v) term" "('f, 'v) term"
| CC_impl "('f, 'v) cond_constraint list" "('f, 'v) cond_constraint"
@@ -142,7 +142,7 @@
type_synonym ('f, 'v, 'w) gsubstL = "('v \<times> ('f, 'w) term) list"
type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL"
-datatype_new (discs_sels) ('f, 'v) cond_constraint_prf =
+datatype (discs_sels) ('f, 'v) cond_constraint_prf =
Final
| Delete_Condition "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
| Different_Constructor "('f, 'v) cond_constraint"
@@ -152,28 +152,28 @@
| Simplify_Condition "('f, 'v) cond_constraint" "('f, 'v) substL" "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
| Induction "('f, 'v) cond_constraint" "('f, 'v) cond_constraint list" "(('f, 'v) rule \<times> (('f, 'v) term \<times> 'v list) list \<times> ('f, 'v) cond_constraint \<times> ('f, 'v) cond_constraint_prf) list"
-datatype_new (discs_sels) ('f, 'v) cond_red_pair_prf =
+datatype (discs_sels) ('f, 'v) cond_red_pair_prf =
Cond_Red_Pair_Prf
'f "(('f, 'v) cond_constraint \<times> ('f, 'v) rules \<times> ('f, 'v) cond_constraint_prf) list" nat nat
-datatype_new (discs_sels) ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
-datatype_new (discs_sels) ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \<times> 'q) list"
-datatype_new (discs_sels) 'q ta_relation =
+datatype (discs_sels) ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
+datatype (discs_sels) ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \<times> 'q) list"
+datatype (discs_sels) 'q ta_relation =
Decision_Proc
| Id_Relation
| Some_Relation "('q \<times> 'q) list"
-datatype_new (discs_sels) boundstype = Roof | Match
-datatype_new (discs_sels) ('f, 'q) bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
+datatype (discs_sels) boundstype = Roof | Match
+datatype (discs_sels) ('f, 'q) bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
-datatype_new (discs_sels) ('f, 'v) pat_eqv_prf =
+datatype (discs_sels) ('f, 'v) pat_eqv_prf =
Pat_Dom_Renaming "('f, 'v) substL"
| Pat_Irrelevant "('f, 'v) substL" "('f, 'v) substL"
| Pat_Simplify "('f, 'v) substL" "('f, 'v) substL"
-datatype_new (discs_sels) pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close
+datatype (discs_sels) pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close
-datatype_new (discs_sels) ('f, 'v) pat_rule_prf =
+datatype (discs_sels) ('f, 'v) pat_rule_prf =
Pat_OrigRule "('f, 'v) rule" bool
| Pat_InitPump "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL"
| Pat_InitPumpCtxt "('f, 'v) pat_rule_prf" "('f, 'v) substL" pos 'v
@@ -183,10 +183,10 @@
| Pat_Rewr "('f, 'v) pat_rule_prf" "('f, 'v) term \<times> ('f, 'v) rseq" pat_rule_pos 'v
| Pat_Exp_Sigma "('f, 'v) pat_rule_prf" nat
-datatype_new (discs_sels) ('f, 'v) non_loop_prf =
+datatype (discs_sels) ('f, 'v) non_loop_prf =
Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos
-datatype_new (discs_sels) ('f, 'l, 'v) problem =
+datatype (discs_sels) ('f, 'l, 'v) problem =
SN_TRS "('f, 'l, 'v) qreltrsLL"
| SN_FP_TRS "('f, 'l, 'v) fptrsLL"
| Finite_DPP "('f, 'l, 'v) dppLL"
@@ -198,7 +198,7 @@
declare [[bnf_timing]]
-datatype_new (discs_sels) ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof =
+datatype (discs_sels) ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof =
SN_assm_proof "('f, 'l, 'v) qreltrsLL" 'a
| Finite_assm_proof "('f, 'l, 'v) dppLL" 'b
| SN_FP_assm_proof "('f, 'l, 'v) fptrsLL" 'c
@@ -210,7 +210,7 @@
type_synonym ('f, 'l, 'v, 'a, 'b, 'c, 'd) assm_proof = "('f, 'l, 'v, 'a, 'b, 'c, dummy_prf, 'd) generic_assm_proof"
-datatype_new (discs_sels) ('f, 'l, 'v) assm =
+datatype (discs_sels) ('f, 'l, 'v) assm =
SN_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) qreltrsLL"
| SN_FP_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) fptrsLL"
| Finite_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) dppLL"
@@ -254,7 +254,7 @@
| "collect_neg_assms tp dpp rtp fptp unk (Unknown_assm_proof p prf) = unk prf"
| "collect_neg_assms tp dpp rtp fptp unk _ = []"
-datatype_new (discs_sels) ('f, 'l, 'v) dp_nontermination_proof =
+datatype (discs_sels) ('f, 'l, 'v) dp_nontermination_proof =
DP_Loop "(('f, 'l) lab, 'v) term" "(('f, 'l) lab, 'v) prseq" "(('f, 'l) lab, 'v) substL" "(('f, 'l) lab, 'v) ctxt"
| DP_Nonloop "(('f, 'l) lab, 'v) non_loop_prf"
| DP_Rule_Removal "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_nontermination_proof"
@@ -312,7 +312,7 @@
('f, 'l, 'v) fp_nontermination_proof,
('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
-datatype_new (discs_sels) ('f, 'l, 'v) dp_termination_proof =
+datatype (discs_sels) ('f, 'l, 'v) dp_termination_proof =
P_is_Empty
| Subterm_Criterion_Proc "('f, 'l) lab projL" "('f, 'l, 'v) rseqL"
"('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
--- a/src/HOL/Datatype_Examples/Lambda_Term.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Datatype_Examples/Lambda_Term.thy Thu Sep 11 19:32:36 2014 +0200
@@ -14,7 +14,7 @@
section {* Datatype definition *}
-datatype_new 'a trm =
+datatype 'a trm =
Var 'a |
App "'a trm" "'a trm" |
Lam 'a "'a trm" |
--- a/src/HOL/Datatype_Examples/Misc_Datatype.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy Thu Sep 11 19:32:36 2014 +0200
@@ -13,26 +13,26 @@
imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/FSet"
begin
-datatype_new (discs_sels) simple = X1 | X2 | X3 | X4
+datatype (discs_sels) simple = X1 | X2 | X3 | X4
-datatype_new (discs_sels) simple' = X1' unit | X2' unit | X3' unit | X4' unit
+datatype (discs_sels) simple' = X1' unit | X2' unit | X3' unit | X4' unit
-datatype_new (discs_sels) simple'' = X1'' nat int | X2''
+datatype (discs_sels) simple'' = X1'' nat int | X2''
-datatype_new (discs_sels) 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
+datatype (discs_sels) 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
-datatype_new (discs_sels) ('b, 'c :: ord, 'd, 'e) some_passive =
+datatype (discs_sels) ('b, 'c :: ord, 'd, 'e) some_passive =
SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
-datatype_new (discs_sels) hfset = HFset "hfset fset"
+datatype (discs_sels) hfset = HFset "hfset fset"
-datatype_new (discs_sels) lambda =
+datatype (discs_sels) lambda =
Var string |
App lambda lambda |
Abs string lambda |
Let "(string \<times> lambda) fset" lambda
-datatype_new (discs_sels) 'a par_lambda =
+datatype (discs_sels) 'a par_lambda =
PVar 'a |
PApp "'a par_lambda" "'a par_lambda" |
PAbs 'a "'a par_lambda" |
@@ -43,70 +43,70 @@
('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
*)
-datatype_new (discs_sels) 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
+datatype (discs_sels) 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
and 'a I2 = I21 | I22 "'a I1" "'a I2"
-datatype_new (discs_sels) 'a tree = TEmpty | TNode 'a "'a forest"
+datatype (discs_sels) 'a tree = TEmpty | TNode 'a "'a forest"
and 'a forest = FNil | FCons "'a tree" "'a forest"
-datatype_new (discs_sels) 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
+datatype (discs_sels) 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
and 'a branch = Branch 'a "'a tree'"
-datatype_new (discs_sels) 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist"
+datatype (discs_sels) 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist"
-datatype_new (discs_sels) ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
+datatype (discs_sels) ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
-datatype_new (discs_sels) 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
+datatype (discs_sels) 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
-datatype_new (discs_sels) ('a, 'b, 'c) some_killing =
+datatype (discs_sels) ('a, 'b, 'c) some_killing =
SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
and ('a, 'b, 'c) in_here =
IH1 'b 'a | IH2 'c
-datatype_new (discs_sels) 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b
-datatype_new (discs_sels) 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
-datatype_new (discs_sels) 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset"
-datatype_new (discs_sels) 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list"
+datatype (discs_sels) 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b
+datatype (discs_sels) 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
+datatype (discs_sels) 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset"
+datatype (discs_sels) 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list"
(*
-datatype_new (discs_sels) 'b fail = F "'b fail" 'b "'b fail" "'b list"
-datatype_new (discs_sels) 'b fail = F "'b fail" 'b "'b fail" 'b
-datatype_new (discs_sels) 'b fail = F1 "'b fail" 'b | F2 "'b fail"
-datatype_new (discs_sels) 'b fail = F "'b fail" 'b
+datatype (discs_sels) 'b fail = F "'b fail" 'b "'b fail" "'b list"
+datatype (discs_sels) 'b fail = F "'b fail" 'b "'b fail" 'b
+datatype (discs_sels) 'b fail = F1 "'b fail" 'b | F2 "'b fail"
+datatype (discs_sels) 'b fail = F "'b fail" 'b
*)
-datatype_new (discs_sels) l1 = L1 "l2 list"
+datatype (discs_sels) l1 = L1 "l2 list"
and l2 = L21 "l1 fset" | L22 l2
-datatype_new (discs_sels) kk1 = KK1 kk2
+datatype (discs_sels) kk1 = KK1 kk2
and kk2 = KK2 kk3
and kk3 = KK3 "kk1 list"
-datatype_new (discs_sels) t1 = T11 t3 | T12 t2
+datatype (discs_sels) t1 = T11 t3 | T12 t2
and t2 = T2 t1
and t3 = T3
-datatype_new (discs_sels) t1' = T11' t2' | T12' t3'
+datatype (discs_sels) t1' = T11' t2' | T12' t3'
and t2' = T2' t1'
and t3' = T3'
(*
-datatype_new (discs_sels) fail1 = F1 fail2
+datatype (discs_sels) fail1 = F1 fail2
and fail2 = F2 fail3
and fail3 = F3 fail1
-datatype_new (discs_sels) fail1 = F1 "fail2 list" fail2
+datatype (discs_sels) fail1 = F1 "fail2 list" fail2
and fail2 = F2 "fail2 fset" fail3
and fail3 = F3 fail1
-datatype_new (discs_sels) fail1 = F1 "fail2 list" fail2
+datatype (discs_sels) fail1 = F1 "fail2 list" fail2
and fail2 = F2 "fail1 fset" fail1
*)
(* SLOW
-datatype_new (discs_sels) ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
+datatype (discs_sels) ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list"
@@ -117,24 +117,24 @@
*)
(* fail:
-datatype_new (discs_sels) tt1 = TT11 tt2 tt3 | TT12 tt2 tt4
+datatype (discs_sels) tt1 = TT11 tt2 tt3 | TT12 tt2 tt4
and tt2 = TT2
and tt3 = TT3 tt4
and tt4 = TT4 tt1
*)
-datatype_new (discs_sels) k1 = K11 k2 k3 | K12 k2 k4
+datatype (discs_sels) k1 = K11 k2 k3 | K12 k2 k4
and k2 = K2
and k3 = K3 k4
and k4 = K4
-datatype_new (discs_sels) tt1 = TT11 tt3 tt2 | TT12 tt2 tt4
+datatype (discs_sels) tt1 = TT11 tt3 tt2 | TT12 tt2 tt4
and tt2 = TT2
and tt3 = TT3 tt1
and tt4 = TT4
(* SLOW
-datatype_new (discs_sels) s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2
+datatype (discs_sels) s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2
and s2 = S21 s7 s5 | S22 s5 s4 s6
and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5
and s4 = S4 s5
@@ -144,35 +144,35 @@
and s8 = S8 nat
*)
-datatype_new (discs_sels) 'a deadbar = DeadBar "'a \<Rightarrow> 'a"
-datatype_new (discs_sels) 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
-datatype_new (discs_sels) ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
-datatype_new (discs_sels) ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
-datatype_new (discs_sels) 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a"
+datatype (discs_sels) 'a deadbar = DeadBar "'a \<Rightarrow> 'a"
+datatype (discs_sels) 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
+datatype (discs_sels) ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
+datatype (discs_sels) ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
+datatype (discs_sels) 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a"
-datatype_new (discs_sels) 'a dead_foo = A
-datatype_new (discs_sels) ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
+datatype (discs_sels) 'a dead_foo = A
+datatype (discs_sels) ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
-datatype_new (discs_sels) d1 = D
-datatype_new (discs_sels) d1' = is_D: D
+datatype (discs_sels) d1 = D
+datatype (discs_sels) d1' = is_D: D
-datatype_new (discs_sels) d2 = D nat
-datatype_new (discs_sels) d2' = is_D: D nat
+datatype (discs_sels) d2 = D nat
+datatype (discs_sels) d2' = is_D: D nat
-datatype_new (discs_sels) d3 = D | E
-datatype_new (discs_sels) d3' = D | is_E: E
-datatype_new (discs_sels) d3'' = is_D: D | E
-datatype_new (discs_sels) d3''' = is_D: D | is_E: E
+datatype (discs_sels) d3 = D | E
+datatype (discs_sels) d3' = D | is_E: E
+datatype (discs_sels) d3'' = is_D: D | E
+datatype (discs_sels) d3''' = is_D: D | is_E: E
-datatype_new (discs_sels) d4 = D nat | E
-datatype_new (discs_sels) d4' = D nat | is_E: E
-datatype_new (discs_sels) d4'' = is_D: D nat | E
-datatype_new (discs_sels) d4''' = is_D: D nat | is_E: E
+datatype (discs_sels) d4 = D nat | E
+datatype (discs_sels) d4' = D nat | is_E: E
+datatype (discs_sels) d4'' = is_D: D nat | E
+datatype (discs_sels) d4''' = is_D: D nat | is_E: E
-datatype_new (discs_sels) d5 = D nat | E int
-datatype_new (discs_sels) d5' = D nat | is_E: E int
-datatype_new (discs_sels) d5'' = is_D: D nat | E int
-datatype_new (discs_sels) d5''' = is_D: D nat | is_E: E int
+datatype (discs_sels) d5 = D nat | E int
+datatype (discs_sels) d5' = D nat | is_E: E int
+datatype (discs_sels) d5'' = is_D: D nat | E int
+datatype (discs_sels) d5''' = is_D: D nat | is_E: E int
instance simple :: countable
by countable_datatype
--- a/src/HOL/Datatype_Examples/Process.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Datatype_Examples/Process.thy Thu Sep 11 19:32:36 2014 +0200
@@ -79,7 +79,7 @@
subsection{* Multi-guard fixpoint definitions, simulated with auxiliary arguments *}
-datatype_new x_y_ax = x | y | ax
+datatype x_y_ax = x | y | ax
primcorec F :: "x_y_ax \<Rightarrow> char list process" where
"xyax = x \<Longrightarrow> isChoice (F xyax)"
@@ -106,7 +106,7 @@
hide_const x y ax X Y AX
(* Process terms *)
-datatype_new ('a,'pvar) process_term =
+datatype ('a,'pvar) process_term =
VAR 'pvar |
PROC "'a process" |
ACT 'a "('a,'pvar) process_term" | CH "('a,'pvar) process_term" "('a,'pvar) process_term"
--- a/src/HOL/Datatype_Examples/Stream_Processor.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Datatype_Examples/Stream_Processor.thy Thu Sep 11 19:32:36 2014 +0200
@@ -14,7 +14,7 @@
section {* Continuous Functions on Streams *}
-datatype_new ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
+datatype ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
codatatype ('a, 'b) sp\<^sub>\<nu> = In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
primrec run\<^sub>\<mu> :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> ('b \<times> 'c) \<times> 'a stream" where
@@ -170,7 +170,7 @@
lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_prod \<theta> id o assl"
unfolding assl_def \<theta>_def F.map_comp comp_def id_apply convol_def map_prod_def split fst_conv snd_conv ..
-datatype_new ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F"
+datatype ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F"
codatatype ('a, 'b) spF\<^sub>\<nu> = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu>")
codatatype 'b JF = Ctor (dtor: "('b, 'b JF) F")
--- a/src/HOL/Decision_Procs/Approximation.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Sep 11 19:32:36 2014 +0200
@@ -2037,7 +2037,7 @@
subsection "Define syntax and semantics"
-datatype_new floatarith
+datatype floatarith
= Add floatarith floatarith
| Minus floatarith
| Mult floatarith floatarith
@@ -2456,7 +2456,7 @@
show ?case by (cases "n < length vs", auto)
qed
-datatype_new form = Bound floatarith floatarith floatarith form
+datatype form = Bound floatarith floatarith floatarith form
| Assign floatarith floatarith form
| Less floatarith floatarith
| LessEqual floatarith floatarith
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Thu Sep 11 19:32:36 2014 +0200
@@ -11,12 +11,12 @@
text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
-datatype_new 'a pol =
+datatype 'a pol =
Pc 'a
| Pinj nat "'a pol"
| PX "'a pol" nat "'a pol"
-datatype_new 'a polex =
+datatype 'a polex =
Pol "'a pol"
| Add "'a polex" "'a polex"
| Sub "'a polex" "'a polex"
--- a/src/HOL/Decision_Procs/Cooper.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Thu Sep 11 19:32:36 2014 +0200
@@ -15,7 +15,7 @@
(**** SHADOW SYNTAX AND SEMANTICS ****)
(*********************************************************************************)
-datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
+datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
| Mul int num
primrec num_size :: "num \<Rightarrow> nat" -- {* A size for num to make inductive proofs simpler *}
@@ -38,7 +38,7 @@
| "Inum bs (Sub a b) = Inum bs a - Inum bs b"
| "Inum bs (Mul c a) = c* Inum bs a"
-datatype_new fm =
+datatype fm =
T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
| Closed nat | NClosed nat
--- a/src/HOL/Decision_Procs/Ferrack.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Sep 11 19:32:36 2014 +0200
@@ -13,7 +13,7 @@
(**** SHADOW SYNTAX AND SEMANTICS ****)
(*********************************************************************************)
-datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
+datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
| Mul int num
(* A size for num to make inductive proofs simpler*)
@@ -36,7 +36,7 @@
| "Inum bs (Sub a b) = Inum bs a - Inum bs b"
| "Inum bs (Mul c a) = (real c) * Inum bs a"
(* FORMULAE *)
-datatype_new fm =
+datatype fm =
T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num|
NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
--- a/src/HOL/Decision_Procs/MIR.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Thu Sep 11 19:32:36 2014 +0200
@@ -105,7 +105,7 @@
(**** SHADOW SYNTAX AND SEMANTICS ****)
(*********************************************************************************)
-datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
+datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
| Mul int num | Floor num| CF int num num
(* A size for num to make inductive proofs simpler*)
@@ -188,7 +188,7 @@
(* FORMULAE *)
-datatype_new fm =
+datatype fm =
T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Sep 11 19:32:36 2014 +0200
@@ -15,7 +15,7 @@
subsection {* Terms *}
-datatype_new tm = CP poly | Bound nat | Add tm tm | Mul poly tm
+datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm
| Neg tm | Sub tm tm | CNP nat poly tm
(* A size for poly to make inductive proofs simpler*)
@@ -493,7 +493,7 @@
subsection{* Formulae *}
-datatype_new fm = T| F| Le tm | Lt tm | Eq tm | NEq tm|
+datatype fm = T| F| Le tm | Lt tm | Eq tm | NEq tm|
NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Sep 11 19:32:36 2014 +0200
@@ -10,7 +10,7 @@
subsection{* Datatype of polynomial expressions *}
-datatype_new poly = C Num | Bound nat | Add poly poly | Sub poly poly
+datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly
| Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
--- a/src/HOL/Enum.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Enum.thy Thu Sep 11 19:32:36 2014 +0200
@@ -493,7 +493,7 @@
text {* We define small finite types for the use in Quickcheck *}
-datatype_new finite_1 = a\<^sub>1
+datatype finite_1 = a\<^sub>1
notation (output) a\<^sub>1 ("a\<^sub>1")
@@ -595,7 +595,7 @@
declare [[simproc del: finite_1_eq]]
hide_const (open) a\<^sub>1
-datatype_new finite_2 = a\<^sub>1 | a\<^sub>2
+datatype finite_2 = a\<^sub>1 | a\<^sub>2
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -701,7 +701,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2
-datatype_new finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
+datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -825,7 +825,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
-datatype_new finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
+datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
@@ -927,7 +927,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
-datatype_new finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
+datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
notation (output) a\<^sub>1 ("a\<^sub>1")
notation (output) a\<^sub>2 ("a\<^sub>2")
--- a/src/HOL/Extraction.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Extraction.thy Thu Sep 11 19:32:36 2014 +0200
@@ -37,7 +37,7 @@
induct_forall_def induct_implies_def induct_equal_def induct_conj_def
induct_true_def induct_false_def
-datatype_new sumbool = Left | Right
+datatype sumbool = Left | Right
subsection {* Type of extracted program *}
--- a/src/HOL/HOLCF/Discrete.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/HOLCF/Discrete.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports Cont
begin
-datatype_new 'a discr = Discr "'a :: type"
+datatype 'a discr = Discr "'a :: type"
subsection {* Discrete cpo class instance *}
--- a/src/HOL/HOLCF/FOCUS/Buffer.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/HOLCF/FOCUS/Buffer.thy Thu Sep 11 19:32:36 2014 +0200
@@ -25,10 +25,10 @@
typedecl D
-datatype_new
+datatype
M = Md D | Mreq ("\<bullet>")
-datatype_new
+datatype
State = Sd D | Snil ("\<currency>")
type_synonym
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports IOA Action Lemmas
begin
-datatype_new 'a abs_action = S 'a | R 'a
+datatype 'a abs_action = S 'a | R 'a
(**********************************************************
--- a/src/HOL/HOLCF/IOA/ABP/Action.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Action.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports Packet
begin
-datatype_new 'm action =
+datatype 'm action =
Next | S_msg 'm | R_msg 'm
| S_pkt "'m packet" | R_pkt "'m packet"
| S_ack bool | R_ack bool
--- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports IOA Action
begin
-datatype_new 'a abs_action = S 'a | R 'a
+datatype 'a abs_action = S 'a | R 'a
definition
ch_asig :: "'a abs_action signature" where
--- a/src/HOL/HOLCF/IOA/NTP/Action.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Action.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports Packet
begin
-datatype_new 'm action = S_msg 'm | R_msg 'm
+datatype 'm action = S_msg 'm | R_msg 'm
| S_pkt "'m packet" | R_pkt "'m packet"
| S_ack bool | R_ack bool
| C_m_s | C_m_r | C_r_s | C_r_r 'm
--- a/src/HOL/HOLCF/IOA/Storage/Action.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/HOLCF/IOA/Storage/Action.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports Main
begin
-datatype_new action = New | Loc nat | Free nat
+datatype action = New | Loc nat | Free nat
lemma [cong]: "!!x. x = y ==> case_action a b c x = case_action a b c y"
by simp
--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports Abstraction
begin
-datatype_new action = INC
+datatype action = INC
definition
C_asig :: "action signature" where
--- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports IOA Abstraction
begin
-datatype_new action = INC
+datatype action = INC
definition
C_asig :: "action signature" where
--- a/src/HOL/HOLCF/Up.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/HOLCF/Up.thy Thu Sep 11 19:32:36 2014 +0200
@@ -13,7 +13,7 @@
subsection {* Definition of new type for lifting *}
-datatype_new 'a u = Ibottom | Iup 'a
+datatype 'a u = Ibottom | Iup 'a
type_notation (xsymbols)
u ("(_\<^sub>\<bottom>)" [1000] 999)
--- a/src/HOL/Hoare/Heap.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Hoare/Heap.thy Thu Sep 11 19:32:36 2014 +0200
@@ -10,7 +10,7 @@
subsection "References"
-datatype_new 'a ref = Null | Ref 'a
+datatype 'a ref = Null | Ref 'a
lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
by (induct x) auto
--- a/src/HOL/Hoare/Hoare_Logic.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy Thu Sep 11 19:32:36 2014 +0200
@@ -15,7 +15,7 @@
type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
-datatype_new 'a com =
+datatype 'a com =
Basic "'a \<Rightarrow> 'a"
| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Thu Sep 11 19:32:36 2014 +0200
@@ -12,7 +12,7 @@
type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
-datatype_new 'a com =
+datatype 'a com =
Basic "'a \<Rightarrow> 'a"
| Abort
| Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60)
--- a/src/HOL/Hoare_Parallel/Graph.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Hoare_Parallel/Graph.thy Thu Sep 11 19:32:36 2014 +0200
@@ -4,7 +4,7 @@
theory Graph imports Main begin
-datatype_new node = Black | White
+datatype node = Black | White
type_synonym nodes = "node list"
type_synonym edge = "nat \<times> nat"
--- a/src/HOL/Hoare_Parallel/OG_Com.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Com.thy Thu Sep 11 19:32:36 2014 +0200
@@ -14,7 +14,7 @@
datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a
com"} for non-annotated commands. *}
-datatype_new 'a ann_com =
+datatype 'a ann_com =
AnnBasic "('a assn)" "('a \<Rightarrow> 'a)"
| AnnSeq "('a ann_com)" "('a ann_com)"
| AnnCond1 "('a assn)" "('a bexp)" "('a ann_com)" "('a ann_com)"
--- a/src/HOL/Hoare_Parallel/RG_Com.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Com.thy Thu Sep 11 19:32:36 2014 +0200
@@ -12,7 +12,7 @@
type_synonym 'a bexp = "'a set"
-datatype_new 'a com =
+datatype 'a com =
Basic "'a \<Rightarrow>'a"
| Seq "'a com" "'a com"
| Cond "'a bexp" "'a com" "'a com"
--- a/src/HOL/IMP/ACom.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/ACom.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Annotated Commands"
-datatype_new 'a acom =
+datatype 'a acom =
SKIP 'a ("SKIP {_}" 61) |
Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
Seq "('a acom)" "('a acom)" ("_;;//_" [60, 61] 60) |
--- a/src/HOL/IMP/AExp.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/AExp.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
type_synonym state = "vname \<Rightarrow> val"
text_raw{*\snip{AExpaexpdef}{2}{1}{% *}
-datatype_new aexp = N int | V vname | Plus aexp aexp
+datatype aexp = N int | V vname | Plus aexp aexp
text_raw{*}%endsnip*}
text_raw{*\snip{AExpavaldef}{1}{2}{% *}
--- a/src/HOL/IMP/ASM.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/ASM.thy Thu Sep 11 19:32:36 2014 +0200
@@ -5,7 +5,7 @@
subsection "Stack Machine"
text_raw{*\snip{ASMinstrdef}{0}{1}{% *}
-datatype_new instr = LOADI val | LOAD vname | ADD
+datatype instr = LOADI val | LOAD vname | ADD
text_raw{*}%endsnip*}
text_raw{*\snip{ASMstackdef}{1}{2}{% *}
--- a/src/HOL/IMP/Abs_Int1_const.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Constant Propagation"
-datatype_new const = Const val | Any
+datatype const = Const val | Any
fun \<gamma>_const where
"\<gamma>_const (Const i) = {i}" |
--- a/src/HOL/IMP/Abs_Int1_parity.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Parity Analysis"
-datatype_new parity = Even | Odd | Either
+datatype parity = Even | Odd | Either
text{* Instantiation of class @{class order} with type @{typ parity}: *}
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Constant Propagation"
-datatype_new cval = Const val | Any
+datatype cval = Const val | Any
fun rep_cval where
"rep_cval (Const n) = {n}" |
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Interval Analysis"
-datatype_new ivl = I "int option" "int option"
+datatype ivl = I "int option" "int option"
text{* We assume an important invariant: arithmetic operations are never
applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j <
--- a/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy Thu Sep 11 19:32:36 2014 +0200
@@ -10,7 +10,7 @@
text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
-datatype_new 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
+datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
fun "fun" where "fun (FunDom f _) = f"
fun dom where "dom (FunDom _ A) = A"
--- a/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Annotated Commands"
-datatype_new 'a acom =
+datatype 'a acom =
SKIP 'a ("SKIP {_}" 61) |
Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
Seq "('a acom)" "('a acom)" ("_;;//_" [60, 61] 60) |
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Constant Propagation"
-datatype_new const = Const val | Any
+datatype const = Const val | Any
fun \<gamma>_const where
"\<gamma>_const (Const n) = {n}" |
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Parity Analysis"
-datatype_new parity = Even | Odd | Either
+datatype parity = Even | Odd | Either
text{* Instantiation of class @{class preord} with type @{typ parity}: *}
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Interval Analysis"
-datatype_new ivl = I "int option" "int option"
+datatype ivl = I "int option" "int option"
definition "\<gamma>_ivl i = (case i of
I (Some l) (Some h) \<Rightarrow> {l..h} |
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy Thu Sep 11 19:32:36 2014 +0200
@@ -10,7 +10,7 @@
text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
-datatype_new 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
+datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
fun "fun" where "fun (FunDom f xs) = f"
fun dom where "dom (FunDom f xs) = xs"
--- a/src/HOL/IMP/BExp.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/BExp.thy Thu Sep 11 19:32:36 2014 +0200
@@ -2,7 +2,7 @@
subsection "Boolean Expressions"
-datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
+datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
text_raw{*\snip{BExpbvaldef}{1}{2}{% *}
fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
--- a/src/HOL/IMP/C_like.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/C_like.thy Thu Sep 11 19:32:36 2014 +0200
@@ -4,14 +4,14 @@
type_synonym state = "nat \<Rightarrow> nat"
-datatype_new aexp = N nat | Deref aexp ("!") | Plus aexp aexp
+datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> nat" where
"aval (N n) s = n" |
"aval (!a) s = s(aval a s)" |
"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"
-datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
+datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
"bval (Bc v) _ = v" |
@@ -20,7 +20,7 @@
"bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"
-datatype_new
+datatype
com = SKIP
| Assign aexp aexp ("_ ::= _" [61, 61] 61)
| New aexp aexp
--- a/src/HOL/IMP/Com.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Com.thy Thu Sep 11 19:32:36 2014 +0200
@@ -2,7 +2,7 @@
theory Com imports BExp begin
-datatype_new
+datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
| Seq com com ("_;;/ _" [60, 61] 60)
--- a/src/HOL/IMP/Compiler.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Compiler.thy Thu Sep 11 19:32:36 2014 +0200
@@ -43,7 +43,7 @@
subsection "Instructions and Stack Machine"
text_raw{*\snip{instrdef}{0}{1}{% *}
-datatype_new instr =
+datatype instr =
LOADI int | LOAD vname | ADD | STORE vname |
JMP int | JMPLESS int | JMPGE int
text_raw{*}%endsnip*}
--- a/src/HOL/IMP/OO.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/OO.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,13 +8,13 @@
where "f(x,y := z) == f(x := (f x)(y := z))"
type_synonym addr = nat
-datatype_new ref = null | Ref addr
+datatype ref = null | Ref addr
type_synonym obj = "string \<Rightarrow> ref"
type_synonym venv = "string \<Rightarrow> ref"
type_synonym store = "addr \<Rightarrow> obj"
-datatype_new exp =
+datatype exp =
Null |
New |
V string |
--- a/src/HOL/IMP/Poly_Types.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Poly_Types.thy Thu Sep 11 19:32:36 2014 +0200
@@ -2,7 +2,7 @@
subsection "Type Variables"
-datatype_new ty = Ity | Rty | TV nat
+datatype ty = Ity | Rty | TV nat
text{* Everything else remains the same. *}
--- a/src/HOL/IMP/Procs.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Procs.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
type_synonym pname = string
-datatype_new
+datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
| Seq com com ("_;;/ _" [60, 61] 60)
--- a/src/HOL/IMP/Types.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/Types.thy Thu Sep 11 19:32:36 2014 +0200
@@ -7,13 +7,13 @@
subsection "Arithmetic Expressions"
-datatype_new val = Iv int | Rv real
+datatype val = Iv int | Rv real
type_synonym vname = string
type_synonym state = "vname \<Rightarrow> val"
text_raw{*\snip{aexptDef}{0}{2}{% *}
-datatype_new aexp = Ic int | Rc real | V vname | Plus aexp aexp
+datatype aexp = Ic int | Rc real | V vname | Plus aexp aexp
text_raw{*}%endsnip*}
inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
@@ -32,7 +32,7 @@
subsection "Boolean Expressions"
-datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
+datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
"tbval (Bc v) s v" |
@@ -44,7 +44,7 @@
subsection "Syntax of Commands"
(* a copy of Com.thy - keep in sync! *)
-datatype_new
+datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
| Seq com com ("_;; _" [60, 61] 60)
@@ -71,7 +71,7 @@
subsection "The Type System"
-datatype_new ty = Ity | Rty
+datatype ty = Ity | Rty
type_synonym tyenv = "vname \<Rightarrow> ty"
--- a/src/HOL/IMP/VCG.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/VCG.thy Thu Sep 11 19:32:36 2014 +0200
@@ -7,7 +7,7 @@
text{* Annotated commands: commands where loops are annotated with
invariants. *}
-datatype_new acom =
+datatype acom =
Askip ("SKIP") |
Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) |
Aseq acom acom ("_;;/ _" [60, 61] 60) |
--- a/src/HOL/IMPP/Com.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMPP/Com.thy Thu Sep 11 19:32:36 2014 +0200
@@ -18,10 +18,10 @@
Arg :: loc and
Res :: loc
-datatype_new vname = Glb glb | Loc loc
+datatype vname = Glb glb | Loc loc
type_synonym globs = "glb => val"
type_synonym locals = "loc => val"
-datatype_new state = st globs locals
+datatype state = st globs locals
(* for the meta theory, the following would be sufficient:
typedecl state
consts st :: "[globs , locals] => state"
@@ -31,7 +31,7 @@
typedecl pname
-datatype_new com
+datatype com
= SKIP
| Ass vname aexp ("_:==_" [65, 65 ] 60)
| Local loc aexp com ("LOCAL _:=_ IN _" [65, 0, 61] 60)
--- a/src/HOL/IMPP/Hoare.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMPP/Hoare.thy Thu Sep 11 19:32:36 2014 +0200
@@ -28,7 +28,7 @@
peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35) where
"peek_and P p = (%Z s. P Z s & p s)"
-datatype_new 'a triple =
+datatype 'a triple =
triple "'a assn" com "'a assn" ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58)
definition
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Sep 11 19:32:36 2014 +0200
@@ -16,7 +16,7 @@
text {* Monadic heap actions either produce values
and transform the heap, or fail *}
-datatype_new 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
+datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
lemma [code, code del]:
"(Code_Evaluation.term_of :: 'a::typerep Heap \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of"
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Thu Sep 11 19:32:36 2014 +0200
@@ -20,7 +20,7 @@
text {* This resembles exactly to Isat's Proof Steps *}
type_synonym Resolvants = "ClauseId * (Lit * ClauseId) list"
-datatype_new ProofStep =
+datatype ProofStep =
ProofDone bool
| Root ClauseId Clause
| Conflict ClauseId Resolvants
--- a/src/HOL/Induct/ABexp.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/ABexp.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports Main
begin
-datatype_new 'a aexp =
+datatype 'a aexp =
IF "'a bexp" "'a aexp" "'a aexp"
| Sum "'a aexp" "'a aexp"
| Diff "'a aexp" "'a aexp"
--- a/src/HOL/Induct/Com.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/Com.thy Thu Sep 11 19:32:36 2014 +0200
@@ -12,7 +12,7 @@
typedecl loc
type_synonym state = "loc => nat"
-datatype_new
+datatype
exp = N nat
| X loc
| Op "nat => nat => nat" exp exp
--- a/src/HOL/Induct/Comb.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/Comb.thy Thu Sep 11 19:32:36 2014 +0200
@@ -20,7 +20,7 @@
text {* Datatype definition of combinators @{text S} and @{text K}. *}
-datatype_new comb = K
+datatype comb = K
| S
| Ap comb comb (infixl "##" 90)
--- a/src/HOL/Induct/Common_Patterns.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/Common_Patterns.thy Thu Sep 11 19:32:36 2014 +0200
@@ -218,7 +218,7 @@
before!
*}
-datatype_new foo = Foo1 nat | Foo2 bar
+datatype foo = Foo1 nat | Foo2 bar
and bar = Bar1 bool | Bar2 bazar
and bazar = Bazar foo
--- a/src/HOL/Induct/Ordinals.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/Ordinals.thy Thu Sep 11 19:32:36 2014 +0200
@@ -14,7 +14,7 @@
@{url "http://www.dcs.ed.ac.uk/home/pgh/chat.html"}).
*}
-datatype_new ordinal =
+datatype ordinal =
Zero
| Succ ordinal
| Limit "nat => ordinal"
--- a/src/HOL/Induct/PropLog.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/PropLog.thy Thu Sep 11 19:32:36 2014 +0200
@@ -20,7 +20,7 @@
subsection {* The datatype of propositions *}
-datatype_new 'a pl =
+datatype 'a pl =
false |
var 'a ("#_" [1000]) |
imp "'a pl" "'a pl" (infixr "->" 90)
--- a/src/HOL/Induct/QuoDataType.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Thu Sep 11 19:32:36 2014 +0200
@@ -10,7 +10,7 @@
subsection{*Defining the Free Algebra*}
text{*Messages with encryption and decryption as free constructors.*}
-datatype_new
+datatype
freemsg = NONCE nat
| MPAIR freemsg freemsg
| CRYPT nat freemsg
--- a/src/HOL/Induct/QuoNestedDataType.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy Thu Sep 11 19:32:36 2014 +0200
@@ -10,7 +10,7 @@
subsection{*Defining the Free Algebra*}
text{*Messages with encryption and decryption as free constructors.*}
-datatype_new
+datatype
freeExp = VAR nat
| PLUS freeExp freeExp
| FNCALL nat "freeExp list"
--- a/src/HOL/Induct/Term.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/Term.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports Main
begin
-datatype_new ('a, 'b) "term" =
+datatype ('a, 'b) "term" =
Var 'a
| App 'b "('a, 'b) term list"
--- a/src/HOL/Induct/Tree.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/Tree.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
imports Main
begin
-datatype_new 'a tree =
+datatype 'a tree =
Atom 'a
| Branch "nat => 'a tree"
@@ -34,7 +34,7 @@
subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
-datatype_new brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
+datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
text{*Addition of ordinals*}
primrec add :: "[brouwer,brouwer] => brouwer"
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Thu Sep 11 19:32:36 2014 +0200
@@ -31,7 +31,7 @@
consisting of variables, constants, and binary operations on
expressions. *}
-datatype_new (dead 'adr, dead 'val) expr =
+datatype (dead 'adr, dead 'val) expr =
Variable 'adr
| Constant 'val
| Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
@@ -51,7 +51,7 @@
text {* Next we model a simple stack machine, with three
instructions. *}
-datatype_new (dead 'adr, dead 'val) instr =
+datatype (dead 'adr, dead 'val) instr =
Const 'val
| Load 'adr
| Apply "'val binop"
--- a/src/HOL/Isar_Examples/Hoare.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy Thu Sep 11 19:32:36 2014 +0200
@@ -21,7 +21,7 @@
type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
-datatype_new 'a com =
+datatype 'a com =
Basic "'a \<Rightarrow> 'a"
| Seq "'a com" "'a com" ("(_;/ _)" [60, 61] 60)
| Cond "'a bexp" "'a com" "'a com"
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
subsection {* Terms and substitution *}
-datatype_new ('a, 'b) "term" =
+datatype ('a, 'b) "term" =
Var 'a
| App 'b "('a, 'b) term list"
--- a/src/HOL/Lattice/Orders.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Lattice/Orders.thy Thu Sep 11 19:32:36 2014 +0200
@@ -46,7 +46,7 @@
of the original one.
*}
-datatype_new 'a dual = dual 'a
+datatype 'a dual = dual 'a
primrec undual :: "'a dual \<Rightarrow> 'a" where
undual_dual: "undual (dual x) = x"
--- a/src/HOL/Lazy_Sequence.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Lazy_Sequence.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
subsection {* Type of lazy sequences *}
-datatype_new (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
+datatype (dead 'a) lazy_sequence = lazy_sequence_of_list "'a list"
primrec list_of_lazy_sequence :: "'a lazy_sequence \<Rightarrow> 'a list"
where
--- a/src/HOL/Library/Extended.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Library/Extended.thy Thu Sep 11 19:32:36 2014 +0200
@@ -10,7 +10,7 @@
"~~/src/HOL/Library/Simps_Case_Conv"
begin
-datatype_new 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
+datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
instantiation extended :: (order)order
--- a/src/HOL/Library/Extended_Real.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy Thu Sep 11 19:32:36 2014 +0200
@@ -20,7 +20,7 @@
subsection {* Definition and basic properties *}
-datatype_new ereal = ereal real | PInfty | MInfty
+datatype ereal = ereal real | PInfty | MInfty
instantiation ereal :: uminus
begin
--- a/src/HOL/Library/IArray.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Library/IArray.thy Thu Sep 11 19:32:36 2014 +0200
@@ -13,7 +13,7 @@
lists first. Arrays could be converted back into lists for printing if they
were wrapped up in an additional constructor. *}
-datatype_new 'a iarray = IArray "'a list"
+datatype 'a iarray = IArray "'a list"
primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
"list_of (IArray xs) = xs"
--- a/src/HOL/Library/Lattice_Constructions.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Library/Lattice_Constructions.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
subsection {* Values extended by a bottom element *}
-datatype_new 'a bot = Value 'a | Bot
+datatype 'a bot = Value 'a | Bot
instantiation bot :: (preorder) preorder
begin
@@ -108,7 +108,7 @@
section {* Values extended by a top element *}
-datatype_new 'a top = Value 'a | Top
+datatype 'a top = Value 'a | Top
instantiation top :: (preorder) preorder
begin
@@ -207,7 +207,7 @@
subsection {* Values extended by a top and a bottom element *}
-datatype_new 'a flat_complete_lattice = Value 'a | Bot | Top
+datatype 'a flat_complete_lattice = Value 'a | Bot | Top
instantiation flat_complete_lattice :: (type) order
begin
--- a/src/HOL/Library/Parallel.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Library/Parallel.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
subsection {* Futures *}
-datatype_new 'a future = fork "unit \<Rightarrow> 'a"
+datatype 'a future = fork "unit \<Rightarrow> 'a"
primrec join :: "'a future \<Rightarrow> 'a" where
"join (fork f) = f ()"
--- a/src/HOL/Library/Phantom_Type.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Library/Phantom_Type.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports Main
begin
-datatype_new ('a, 'b) phantom = phantom 'b
+datatype ('a, 'b) phantom = phantom 'b
primrec of_phantom :: "('a, 'b) phantom \<Rightarrow> 'b"
where "of_phantom (phantom x) = x"
--- a/src/HOL/Library/RBT_Impl.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Thu Sep 11 19:32:36 2014 +0200
@@ -16,8 +16,8 @@
subsection {* Datatype of RB trees *}
-datatype_new color = R | B
-datatype_new ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
+datatype color = R | B
+datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
lemma rbt_cases:
obtains (Empty) "t = Empty"
@@ -1728,7 +1728,7 @@
where
"skip_black t = (let t' = skip_red t in case t' of Branch color.B l k v r \<Rightarrow> l | _ \<Rightarrow> t')"
-datatype_new compare = LT | GT | EQ
+datatype compare = LT | GT | EQ
partial_function (tailrec) compare_height :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> compare"
where
--- a/src/HOL/Library/Tree.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Library/Tree.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
imports Main
begin
-datatype_new 'a tree = Leaf | Node (left: "'a tree") (val: 'a) (right: "'a tree")
+datatype 'a tree = Leaf | Node (left: "'a tree") (val: 'a) (right: "'a tree")
where
"left Leaf = Leaf"
| "right Leaf = Leaf"
--- a/src/HOL/List.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/List.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports Sledgehammer Code_Numeral Lifting_Set Lifting_Option Lifting_Product
begin
-datatype_new (set: 'a) list =
+datatype (set: 'a) list =
Nil ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
for
--- a/src/HOL/Metis_Examples/Binary_Tree.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy Thu Sep 11 19:32:36 2014 +0200
@@ -13,7 +13,7 @@
declare [[metis_new_skolem]]
-datatype_new 'a bt =
+datatype 'a bt =
Lf
| Br 'a "'a bt" "'a bt"
--- a/src/HOL/Metis_Examples/Message.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Metis_Examples/Message.thy Thu Sep 11 19:32:36 2014 +0200
@@ -34,10 +34,10 @@
definition symKeys :: "key set" where
"symKeys == {K. invKey K = K}"
-datatype_new --{*We allow any number of friendly agents*}
+datatype --{*We allow any number of friendly agents*}
agent = Server | Friend nat | Spy
-datatype_new
+datatype
msg = Agent agent --{*Agent names*}
| Number nat --{*Ordinary integers, timestamps, ...*}
| Nonce nat --{*Unguessable nonces*}
--- a/src/HOL/Metis_Examples/Trans_Closure.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy Thu Sep 11 19:32:36 2014 +0200
@@ -15,7 +15,7 @@
type_synonym addr = nat
-datatype_new val
+datatype val
= Unit -- "dummy result value of void expressions"
| Null -- "null reference"
| Bool bool -- "Boolean value"
--- a/src/HOL/MicroJava/DFA/Err.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/MicroJava/DFA/Err.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
imports Semilat
begin
-datatype_new 'a err = Err | OK 'a
+datatype 'a err = Err | OK 'a
type_synonym 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
type_synonym 'a esl = "'a set * 'a ord * 'a ebinop"
--- a/src/HOL/MicroJava/J/Example.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Thu Sep 11 19:32:36 2014 +0200
@@ -36,8 +36,8 @@
\end{verbatim}
*}
-datatype_new cnam' = Base' | Ext'
-datatype_new vnam' = vee' | x' | e'
+datatype cnam' = Base' | Ext'
+datatype vnam' = vee' | x' | e'
text {*
@{text cnam'} and @{text vnam'} are intended to be isomorphic
--- a/src/HOL/MicroJava/J/Term.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/MicroJava/J/Term.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,9 +6,9 @@
theory Term imports Value begin
-datatype_new binop = Eq | Add -- "function codes for binary operation"
+datatype binop = Eq | Add -- "function codes for binary operation"
-datatype_new expr
+datatype expr
= NewC cname -- "class instance creation"
| Cast cname expr -- "type cast"
| Lit val -- "literal value, also references"
@@ -23,7 +23,7 @@
datatype_compat expr
-datatype_new stmt
+datatype stmt
= Skip -- "empty statement"
| Expr expr -- "expression statement"
| Comp stmt stmt ("_;; _" [61,60]60)
--- a/src/HOL/MicroJava/J/Type.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/MicroJava/J/Type.thy Thu Sep 11 19:32:36 2014 +0200
@@ -45,14 +45,14 @@
end
-- "exceptions"
-datatype_new
+datatype
xcpt
= NullPointer
| ClassCast
| OutOfMemory
-- "class names"
-datatype_new cname
+datatype cname
= Object
| Xcpt xcpt
| Cname cnam
@@ -128,23 +128,23 @@
end
-- "names for @{text This} pointer and local/field variables"
-datatype_new vname
+datatype vname
= This
| VName vnam
-- "primitive type, cf. 4.2"
-datatype_new prim_ty
+datatype prim_ty
= Void -- "'result type' of void methods"
| Boolean
| Integer
-- "reference type, cf. 4.3"
-datatype_new ref_ty
+datatype ref_ty
= NullT -- "null type, cf. 4.1"
| ClassT cname -- "class type"
-- "any type, cf. 4.1"
-datatype_new ty
+datatype ty
= PrimT prim_ty -- "primitive type"
| RefT ref_ty -- "reference type"
--- a/src/HOL/MicroJava/J/Value.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/MicroJava/J/Value.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,11 +8,11 @@
typedecl loc' -- "locations, i.e. abstract references on objects"
-datatype_new loc
+datatype loc
= XcptRef xcpt -- "special locations for pre-allocated system exceptions"
| Loc loc' -- "usual locations (references on objects)"
-datatype_new val
+datatype val
= Unit -- "dummy result value of void methods"
| Null -- "null reference"
| Bool bool -- "Boolean value"
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Thu Sep 11 19:32:36 2014 +0200
@@ -11,7 +11,7 @@
text {*
Extend the state space by one element indicating a type error (or
other abnormal termination) *}
-datatype_new 'a type_error = TypeError | Normal 'a
+datatype 'a type_error = TypeError | Normal 'a
abbreviation
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
theory JVMInstructions imports JVMState begin
-datatype_new
+datatype
instr = Load nat -- "load from local variable"
| Store nat -- "store into local variable"
| LitPush val -- "push a literal (constant)"
--- a/src/HOL/NanoJava/Decl.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/NanoJava/Decl.thy Thu Sep 11 19:32:36 2014 +0200
@@ -7,7 +7,7 @@
theory Decl imports Term begin
-datatype_new ty
+datatype ty
= NT --{* null type *}
| Class cname --{* class type *}
--- a/src/HOL/NanoJava/State.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/NanoJava/State.thy Thu Sep 11 19:32:36 2014 +0200
@@ -13,7 +13,7 @@
text {* Locations, i.e.\ abstract references to objects *}
typedecl loc
-datatype_new val
+datatype val
= Null --{* null reference *}
| Addr loc --{* address, i.e. location of object *}
--- a/src/HOL/NanoJava/Term.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/NanoJava/Term.thy Thu Sep 11 19:32:36 2014 +0200
@@ -23,7 +23,7 @@
Res_neq_This [simp]: "Res \<noteq> This"
*)
-datatype_new stmt
+datatype stmt
= Skip --{* empty statement *}
| Comp stmt stmt ("_;; _" [91,90 ] 90)
| Cond expr stmt stmt ("If '(_') _ Else _" [ 3,91,91] 91)
--- a/src/HOL/Nitpick.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Nitpick.thy Thu Sep 11 19:32:36 2014 +0200
@@ -14,9 +14,9 @@
"nitpick_params" :: thy_decl
begin
-datatype_new (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
-datatype_new (dead 'a, dead 'b) pair_box = PairBox 'a 'b
-datatype_new (dead 'a) word = Word "'a set"
+datatype (dead 'a, dead 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
+datatype (dead 'a, dead 'b) pair_box = PairBox 'a 'b
+datatype (dead 'a) word = Word "'a set"
typedecl bisim_iterator
typedecl unsigned_bit
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Thu Sep 11 19:32:36 2014 +0200
@@ -44,7 +44,7 @@
nitpick [card = 17, expect = none]
oops
-datatype_new ('a, 'b) pd = Pd "'a \<times> 'b"
+datatype ('a, 'b) pd = Pd "'a \<times> 'b"
fun fs where
"fs (Pd (a, _)) = a"
@@ -76,7 +76,7 @@
nitpick [expect = genuine]
oops
-datatype_new ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
+datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
fun app where
"app (Fn f) x = f x"
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Thu Sep 11 19:32:36 2014 +0200
@@ -206,7 +206,7 @@
nitpick [binary_ints, expect = none]
sorry
-datatype_new tree = Null | Node nat tree tree
+datatype tree = Null | Node nat tree tree
primrec labels where
"labels Null = {}" |
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Sep 11 19:32:36 2014 +0200
@@ -223,7 +223,7 @@
subsection {* 2.10. Boxing *}
-datatype_new tm = Var nat | Lam tm | App tm tm
+datatype tm = Var nat | Lam tm | App tm tm
primrec lift where
"lift (Var j) k = Var (if j < k then j else j + 1)" |
@@ -306,7 +306,7 @@
subsection {* 3.1. A Context-Free Grammar *}
-datatype_new alphabet = a | b
+datatype alphabet = a | b
inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
"[] \<in> S\<^sub>1"
@@ -381,7 +381,7 @@
subsection {* 3.2. AA Trees *}
-datatype_new 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
+datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
primrec data where
"data \<Lambda> = undefined" |
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Thu Sep 11 19:32:36 2014 +0200
@@ -617,7 +617,7 @@
text {* Non-recursive datatypes *}
-datatype_new T1 = A | B
+datatype T1 = A | B
lemma "P (x\<Colon>T1)"
nitpick [expect = genuine]
@@ -653,7 +653,7 @@
nitpick [expect = genuine]
oops
-datatype_new 'a T2 = C T1 | D 'a
+datatype 'a T2 = C T1 | D 'a
lemma "P (x\<Colon>'a T2)"
nitpick [expect = genuine]
@@ -685,7 +685,7 @@
nitpick [expect = genuine]
oops
-datatype_new ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
+datatype ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
lemma "P (x\<Colon>('a, 'b) T3)"
nitpick [expect = genuine]
@@ -790,7 +790,7 @@
nitpick [expect = genuine]
oops
-datatype_new BitList = BitListNil | Bit0 BitList | Bit1 BitList
+datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
lemma "P (x\<Colon>BitList)"
nitpick [expect = genuine]
@@ -823,7 +823,7 @@
nitpick [expect = genuine]
oops
-datatype_new 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
+datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
lemma "P (x\<Colon>'a BinTree)"
nitpick [expect = genuine]
@@ -857,7 +857,7 @@
text {* Mutually recursive datatypes *}
-datatype_new 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
+datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
and 'a bexp = Equal "'a aexp" "'a aexp"
lemma "P (x\<Colon>'a aexp)"
@@ -911,7 +911,7 @@
nitpick [expect = genuine]
oops
-datatype_new X = A | B X | C Y and Y = D X | E Y | F
+datatype X = A | B X | C Y and Y = D X | E Y | F
lemma "P (x\<Colon>X)"
nitpick [expect = genuine]
@@ -999,7 +999,7 @@
text {* Indirect recursion is implemented via mutual recursion. *}
-datatype_new XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
+datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
lemma "P (x\<Colon>XOpt)"
nitpick [expect = genuine]
@@ -1017,7 +1017,7 @@
nitpick [expect = genuine]
oops
-datatype_new 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
+datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
lemma "P (x\<Colon>'a YOpt)"
nitpick [expect = genuine]
@@ -1031,7 +1031,7 @@
nitpick [expect = genuine]
oops
-datatype_new Trie = TR "Trie list"
+datatype Trie = TR "Trie list"
lemma "P (x\<Colon>Trie)"
nitpick [expect = genuine]
@@ -1045,7 +1045,7 @@
nitpick [expect = genuine]
oops
-datatype_new InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
+datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
lemma "P (x\<Colon>InfTree)"
nitpick [expect = genuine]
@@ -1073,7 +1073,7 @@
nitpick [expect = genuine]
oops
-datatype_new 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
+datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
lemma "P (x\<Colon>'a lambda)"
nitpick [expect = genuine]
@@ -1109,8 +1109,8 @@
text {* Taken from "Inductive datatypes in HOL", p. 8: *}
-datatype_new (dead 'a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
-datatype_new 'c U = E "('c, 'c U) T"
+datatype (dead 'a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
+datatype 'c U = E "('c, 'c U) T"
lemma "P (x\<Colon>'c U)"
nitpick [expect = genuine]
--- a/src/HOL/Nominal/Examples/CK_Machine.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy Thu Sep 11 19:32:36 2014 +0200
@@ -81,7 +81,7 @@
section {* Evaluation Contexts *}
-datatype_new ctx =
+datatype ctx =
Hole ("\<box>")
| CAPPL "ctx" "lam"
| CAPPR "lam" "ctx"
--- a/src/HOL/Nominal/Examples/Pattern.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy Thu Sep 11 19:32:36 2014 +0200
@@ -38,7 +38,7 @@
where
"\<lambda>x:T. t \<equiv> Abs T x t"
-datatype_new pat =
+datatype pat =
PVar name ty
| PTuple pat pat ("(1'\<langle>\<langle>_,/ _'\<rangle>\<rangle>)")
--- a/src/HOL/Nominal/Nominal.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Nominal/Nominal.thy Thu Sep 11 19:32:36 2014 +0200
@@ -18,12 +18,12 @@
swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
(* a "private" copy of the option type used in the abstraction function *)
-datatype_new 'a noption = nSome 'a | nNone
+datatype 'a noption = nSome 'a | nNone
datatype_compat noption
(* a "private" copy of the product type used in the nominal induct method *)
-datatype_new ('a, 'b) nprod = nPair 'a 'b
+datatype ('a, 'b) nprod = nPair 'a 'b
datatype_compat nprod
--- a/src/HOL/Num.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Num.thy Thu Sep 11 19:32:36 2014 +0200
@@ -11,7 +11,7 @@
subsection {* The @{text num} type *}
-datatype_new num = One | Bit0 num | Bit1 num
+datatype num = One | Bit0 num | Bit1 num
text {* Increment function for type @{typ num} *}
--- a/src/HOL/Option.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Option.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports BNF_Least_Fixpoint Finite_Set
begin
-datatype_new 'a option =
+datatype 'a option =
None
| Some (the: 'a)
--- a/src/HOL/Predicate.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate.thy Thu Sep 11 19:32:36 2014 +0200
@@ -10,7 +10,7 @@
subsection {* The type of predicate enumerations (a monad) *}
-datatype_new 'a pred = Pred "'a \<Rightarrow> bool"
+datatype 'a pred = Pred "'a \<Rightarrow> bool"
primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where
eval_pred: "eval (Pred f) = f"
@@ -402,7 +402,7 @@
subsection {* Implementation *}
-datatype_new 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
+datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where
"pred_of_seq Empty = \<bottom>"
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 11 19:32:36 2014 +0200
@@ -107,7 +107,7 @@
hide_const Pow
-datatype_new expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
+datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
| Minus expr expr | Uminus expr | Pow expr int | Exp expr
text {*
@@ -197,7 +197,7 @@
section {* Example negation *}
-datatype_new abc = A | B | C
+datatype abc = A | B | C
inductive notB :: "abc => bool"
where
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Thu Sep 11 19:32:36 2014 +0200
@@ -24,7 +24,7 @@
(Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
*}
-datatype_new alphabet = a | b
+datatype alphabet = a | b
inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
"[] \<in> S\<^sub>1"
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy Thu Sep 11 19:32:36 2014 +0200
@@ -10,11 +10,11 @@
text {* a contribution by Aditi Barthwal *}
-datatype_new ('nts,'ts) symbol = NTS 'nts
+datatype ('nts,'ts) symbol = NTS 'nts
| TS 'ts
-datatype_new ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"
+datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"
type_synonym ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts"
@@ -75,7 +75,7 @@
subsection {* Some concrete Context Free Grammars *}
-datatype_new alphabet = a | b
+datatype alphabet = a | b
inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
"[] \<in> S\<^sub>1"
@@ -140,7 +140,7 @@
type_synonym var = nat
type_synonym state = "int list"
-datatype_new com =
+datatype com =
Skip |
Ass var "state => int" |
Seq com com |
@@ -164,11 +164,11 @@
subsection {* Lambda *}
-datatype_new type =
+datatype type =
Atom nat
| Fun type type (infixr "\<Rightarrow>" 200)
-datatype_new dB =
+datatype dB =
Var nat
| App dB dB (infixl "\<degree>" 200)
| Abs type dB
@@ -237,12 +237,12 @@
type_synonym vvalue = int
type_synonym var_assign = "vname \<Rightarrow> vvalue" --"variable assignment"
-datatype_new ir_expr =
+datatype ir_expr =
IrConst vvalue
| ObjAddr vname
| Add ir_expr ir_expr
-datatype_new val =
+datatype val =
IntVal vvalue
record configuration =
@@ -267,14 +267,14 @@
type_synonym name = nat --"For simplicity in examples"
type_synonym state' = "name \<Rightarrow> nat"
-datatype_new aexp = N nat | V name | Plus aexp aexp
+datatype aexp = N nat | V name | Plus aexp aexp
fun aval :: "aexp \<Rightarrow> state' \<Rightarrow> nat" where
"aval (N n) _ = n" |
"aval (V x) st = st x" |
"aval (Plus e\<^sub>1 e\<^sub>2) st = aval e\<^sub>1 st + aval e\<^sub>2 st"
-datatype_new bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
+datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
primrec bval :: "bexp \<Rightarrow> state' \<Rightarrow> bool" where
"bval (B b) _ = b" |
@@ -282,7 +282,7 @@
"bval (And b1 b2) st = (bval b1 st \<and> bval b2 st)" |
"bval (Less a\<^sub>1 a\<^sub>2) st = (aval a\<^sub>1 st < aval a\<^sub>2 st)"
-datatype_new
+datatype
com' = SKIP
| Assign name aexp ("_ ::= _" [1000, 61] 61)
| Semi com' com' ("_; _" [60, 61] 60)
@@ -326,7 +326,7 @@
text{* This example formalizes finite CCS processes without communication or
recursion. For simplicity, labels are natural numbers. *}
-datatype_new proc = nil | pre nat proc | or proc proc | par proc proc
+datatype proc = nil | pre nat proc | or proc proc | par proc proc
inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
"step (pre n p) n p" |
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Sep 11 19:32:36 2014 +0200
@@ -2,13 +2,13 @@
imports Main
begin
-datatype_new guest = Guest0 | Guest1
-datatype_new key = Key0 | Key1 | Key2 | Key3
-datatype_new room = Room0
+datatype guest = Guest0 | Guest1
+datatype key = Key0 | Key1 | Key2 | Key3
+datatype room = Room0
type_synonym card = "key * key"
-datatype_new event =
+datatype event =
Check_in guest room card | Enter guest room card | Exit guest room
definition initk :: "room \<Rightarrow> key"
--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy Thu Sep 11 19:32:36 2014 +0200
@@ -11,7 +11,7 @@
type_synonym var = unit
type_synonym state = bool
-datatype_new com =
+datatype com =
Skip |
Ass bool |
Seq com com |
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Thu Sep 11 19:32:36 2014 +0200
@@ -11,7 +11,7 @@
type_synonym var = unit
type_synonym state = bool
-datatype_new com =
+datatype com =
Skip |
Ass bool |
Seq com com |
--- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy Thu Sep 11 19:32:36 2014 +0200
@@ -11,7 +11,7 @@
type_synonym var = unit
type_synonym state = int
-datatype_new com =
+datatype com =
Skip |
Ass var "int" |
Seq com com |
--- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy Thu Sep 11 19:32:36 2014 +0200
@@ -11,7 +11,7 @@
type_synonym var = nat
type_synonym state = "int list"
-datatype_new com =
+datatype com =
Skip |
Ass var "int" |
Seq com com |
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 11 19:32:36 2014 +0200
@@ -4,11 +4,11 @@
subsection {* Lambda *}
-datatype_new type =
+datatype type =
Atom nat
| Fun type type (infixr "\<Rightarrow>" 200)
-datatype_new dB =
+datatype dB =
Var nat
| App dB dB (infixl "\<degree>" 200)
| Abs type dB
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Thu Sep 11 19:32:36 2014 +0200
@@ -53,7 +53,7 @@
section {* Context Free Grammar *}
-datatype_new alphabet = a | b
+datatype alphabet = a | b
inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
"[] \<in> S\<^sub>1"
@@ -179,7 +179,7 @@
type_synonym var = nat
type_synonym state = "int list"
-datatype_new com =
+datatype com =
Skip |
Ass var "int" |
Seq com com |
@@ -206,11 +206,11 @@
subsection {* Lambda *}
-datatype_new type =
+datatype type =
Atom nat
| Fun type type (infixr "\<Rightarrow>" 200)
-datatype_new dB =
+datatype dB =
Var nat
| App dB dB (infixl "\<degree>" 200)
| Abs type dB
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Sep 11 19:32:36 2014 +0200
@@ -139,7 +139,7 @@
subsection {* Alternative Rules *}
-datatype_new char = C | D | E | F | G | H
+datatype char = C | D | E | F | G | H
inductive is_C_or_D
where
@@ -784,7 +784,7 @@
type_synonym var = nat
type_synonym state = "int list"
-datatype_new com =
+datatype com =
Skip |
Ass var "state => int" |
Seq com com |
@@ -809,7 +809,7 @@
text{* This example formalizes finite CCS processes without communication or
recursion. For simplicity, labels are natural numbers. *}
-datatype_new proc = nil | pre nat proc | or proc proc | par proc proc
+datatype proc = nil | pre nat proc | or proc proc | par proc proc
inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
where
@@ -974,7 +974,7 @@
*)
subsection {* AVL Tree *}
-datatype_new 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
+datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
fun height :: "'a tree => nat" where
"height ET = 0"
| "height (MKT x l r h) = max (height l) (height r) + 1"
@@ -1403,7 +1403,7 @@
thm is_error'.equation
-datatype_new ErrorObject = Error String.literal int
+datatype ErrorObject = Error String.literal int
inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
where
@@ -1508,7 +1508,7 @@
text {* The higher-order predicate r is in an output term *}
-datatype_new result = Result bool
+datatype result = Result bool
inductive fixed_relation :: "'a => bool"
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
manually slightly adapted.
*}
-datatype_new Nat = Zer
+datatype Nat = Zer
| Suc Nat
fun sub :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat"
@@ -20,10 +20,10 @@
Zer \<Rightarrow> Zer
| Suc x' \<Rightarrow> sub x' y')"
-datatype_new Sym = N0
+datatype Sym = N0
| N1 Sym
-datatype_new RE = Sym Sym
+datatype RE = Sym Sym
| Or RE RE
| Seq RE RE
| And RE RE
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Thu Sep 11 19:32:36 2014 +0200
@@ -107,13 +107,13 @@
"unique [] = True"
| "unique (x # xs) = (xs\<langle>fst x\<rangle>\<^sub>? = \<bottom> \<and> unique xs)"
-datatype_new type =
+datatype type =
TVar nat
| Top
| Fun type type (infixr "\<rightarrow>" 200)
| TyAll type type ("(3\<forall><:_./ _)" [0, 10] 10)
-datatype_new binding = VarB type | TVarB type
+datatype binding = VarB type | TVarB type
type_synonym env = "binding list"
primrec is_TVarB :: "binding \<Rightarrow> bool"
@@ -131,7 +131,7 @@
"mapB f (VarB T) = VarB (f T)"
| "mapB f (TVarB T) = TVarB (f T)"
-datatype_new trm =
+datatype trm =
Var nat
| Abs type trm ("(3\<lambda>:_./ _)" [0, 10] 10)
| TAbs type trm ("(3\<lambda><:_./ _)" [0, 10] 10)
--- a/src/HOL/Proofs/Extraction/Higman.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Proofs/Extraction/Higman.thy Thu Sep 11 19:32:36 2014 +0200
@@ -14,7 +14,7 @@
based on Coquand and Fridlender \cite{Coquand93}.
*}
-datatype_new letter = A | B
+datatype letter = A | B
inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"
where
--- a/src/HOL/Proofs/Extraction/Warshall.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Proofs/Extraction/Warshall.thy Thu Sep 11 19:32:36 2014 +0200
@@ -13,7 +13,7 @@
based on Berger, Schwichtenberg and Seisenberger \cite{Berger-JAR-2001}.
*}
-datatype_new b = T | F
+datatype b = T | F
primrec
is_path' :: "('a \<Rightarrow> 'a \<Rightarrow> b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
--- a/src/HOL/Proofs/Lambda/Lambda.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Proofs/Lambda/Lambda.thy Thu Sep 11 19:32:36 2014 +0200
@@ -12,7 +12,7 @@
subsection {* Lambda-terms in de Bruijn notation and substitution *}
-datatype_new dB =
+datatype dB =
Var nat
| App dB dB (infixl "\<degree>" 200)
| Abs dB
--- a/src/HOL/Proofs/Lambda/LambdaType.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Proofs/Lambda/LambdaType.thy Thu Sep 11 19:32:36 2014 +0200
@@ -35,7 +35,7 @@
subsection {* Types and typing rules *}
-datatype_new type =
+datatype type =
Atom nat
| Fun type type (infixr "\<Rightarrow>" 200)
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Thu Sep 11 19:32:36 2014 +0200
@@ -2,7 +2,7 @@
imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
begin
-datatype_new agent = Alice | Bob | Spy
+datatype agent = Alice | Bob | Spy
definition agents :: "agent set"
where
@@ -12,14 +12,14 @@
where
"bad = {Spy}"
-datatype_new key = pubEK agent | priEK agent
+datatype key = pubEK agent | priEK agent
fun invKey
where
"invKey (pubEK A) = priEK A"
| "invKey (priEK A) = pubEK A"
-datatype_new
+datatype
msg = Agent agent
| Key key
| Nonce nat
@@ -73,7 +73,7 @@
| initState_Spy:
"initState Spy = (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)"
-datatype_new
+datatype
event = Says agent agent msg
| Gets agent msg
| Notes agent msg
--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy Thu Sep 11 19:32:36 2014 +0200
@@ -2,13 +2,13 @@
imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
begin
-datatype_new guest = Guest0 | Guest1
-datatype_new key = Key0 | Key1 | Key2 | Key3
-datatype_new room = Room0
+datatype guest = Guest0 | Guest1
+datatype key = Key0 | Key1 | Key2 | Key3
+datatype room = Room0
type_synonym card = "key * key"
-datatype_new event =
+datatype event =
Check_in guest room card
| Enter guest room card
| Exit guest room
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Thu Sep 11 19:32:36 2014 +0200
@@ -122,7 +122,7 @@
subsection {* Trees *}
-datatype_new 'a tree = Twig | Leaf 'a | Branch "'a tree" "'a tree"
+datatype 'a tree = Twig | Leaf 'a | Branch "'a tree" "'a tree"
primrec leaves :: "'a tree \<Rightarrow> 'a list" where
"leaves Twig = []"
@@ -150,7 +150,7 @@
--{* Wrong! *}
oops
-datatype_new 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
+datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
"inOrder (Tip a)= [a]"
@@ -439,7 +439,7 @@
quickcheck[random, expect = counterexample]
oops
-datatype_new colour = Red | Green | Blue
+datatype colour = Red | Green | Blue
record cpoint = point +
colour :: colour
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy Thu Sep 11 19:32:36 2014 +0200
@@ -132,7 +132,7 @@
subsection {* AVL Trees *}
-datatype_new 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
+datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
primrec set_of :: "'a tree \<Rightarrow> 'a set"
where
--- a/src/HOL/Quickcheck_Exhaustive.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Thu Sep 11 19:32:36 2014 +0200
@@ -574,8 +574,8 @@
where
"pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
-datatype_new (dead 'a) unknown = Unknown | Known 'a
-datatype_new (dead 'a) three_valued = Unknown_value | Value 'a | No_value
+datatype (dead 'a) unknown = Unknown | Known 'a
+datatype (dead 'a) three_valued = Unknown_value | Value 'a | No_value
type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued"
--- a/src/HOL/Quickcheck_Narrowing.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Thu Sep 11 19:32:36 2014 +0200
@@ -26,14 +26,14 @@
subsubsection {* Narrowing's deep representation of types and terms *}
-datatype_new narrowing_type =
+datatype narrowing_type =
Narrowing_sum_of_products "narrowing_type list list"
-datatype_new narrowing_term =
+datatype narrowing_term =
Narrowing_variable "integer list" narrowing_type
| Narrowing_constructor integer "narrowing_term list"
-datatype_new (dead 'a) narrowing_cons =
+datatype (dead 'a) narrowing_cons =
Narrowing_cons narrowing_type "(narrowing_term list \<Rightarrow> 'a) list"
primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
@@ -127,7 +127,7 @@
class narrowing =
fixes narrowing :: "integer => 'a narrowing_cons"
-datatype_new property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
+datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
(* FIXME: hard-wired maximal depth of 100 here *)
definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
@@ -155,7 +155,7 @@
subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
-datatype_new (dead 'a, dead 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
+datatype (dead 'a, dead 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b"
where
@@ -165,7 +165,7 @@
hide_type (open) ffun
hide_const (open) Constant Update eval_ffun
-datatype_new (dead 'b) cfun = Constant 'b
+datatype (dead 'b) cfun = Constant 'b
primrec eval_cfun :: "'b cfun => 'a => 'b"
where
--- a/src/HOL/Quotient_Examples/Quotient_Message.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Thu Sep 11 19:32:36 2014 +0200
@@ -10,7 +10,7 @@
subsection{*Defining the Free Algebra*}
-datatype_new
+datatype
freemsg = NONCE nat
| MPAIR freemsg freemsg
| CRYPT nat freemsg
--- a/src/HOL/Record.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Record.thy Thu Sep 11 19:32:36 2014 +0200
@@ -79,7 +79,7 @@
subsection {* Operators and lemmas for types isomorphic to tuples *}
-datatype_new (dead 'a, dead 'b, dead 'c) tuple_isomorphism =
+datatype (dead 'a, dead 'b, dead 'c) tuple_isomorphism =
Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
primrec
--- a/src/HOL/SET_Protocol/Event_SET.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/SET_Protocol/Event_SET.thy Thu Sep 11 19:32:36 2014 +0200
@@ -15,7 +15,7 @@
text{*Message events*}
-datatype_new
+datatype
event = Says agent agent msg
| Gets agent msg
| Notes agent msg
--- a/src/HOL/SET_Protocol/Message_SET.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Thu Sep 11 19:32:36 2014 +0200
@@ -52,11 +52,11 @@
text{*Agents. We allow any number of certification authorities, cardholders
merchants, and payment gateways.*}
-datatype_new
+datatype
agent = CA nat | Cardholder nat | Merchant nat | PG nat | Spy
text{*Messages*}
-datatype_new
+datatype
msg = Agent agent --{*Agent names*}
| Number nat --{*Ordinary integers, timestamps, ...*}
| Nonce nat --{*Unguessable nonces*}
--- a/src/HOL/SPARK/Manual/Complex_Types.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/SPARK/Manual/Complex_Types.thy Thu Sep 11 19:32:36 2014 +0200
@@ -2,7 +2,7 @@
imports "../SPARK"
begin
-datatype_new day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
+datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
record two_fields =
Field1 :: "int \<times> day \<Rightarrow> int"
--- a/src/HOL/Statespace/DistinctTreeProver.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Thu Sep 11 19:32:36 2014 +0200
@@ -18,7 +18,7 @@
subsection {* The Binary Tree *}
-datatype_new 'a tree = Node "'a tree" 'a bool "'a tree" | Tip
+datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip
text {* The boolean flag in the node marks the content of the node as
--- a/src/HOL/String.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/String.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
subsection {* Characters and strings *}
-datatype_new nibble =
+datatype nibble =
Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
| Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
@@ -114,7 +114,7 @@
"nibble_of_nat (n mod 16) = nibble_of_nat n"
by (simp add: nibble_of_nat_def)
-datatype_new char = Char nibble nibble
+datatype char = Char nibble nibble
-- "Note: canonical order of character encoding coincides with standard term ordering"
syntax
--- a/src/HOL/TLA/Inc/Inc.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
begin
(* program counter as an enumeration type *)
-datatype_new pcount = a | b | g
+datatype pcount = a | b | g
axiomatization
(* program variables *)
--- a/src/HOL/TLA/Memory/MemClerkParameters.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/TLA/Memory/MemClerkParameters.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports RPCParameters
begin
-datatype_new mClkState = clkA | clkB
+datatype mClkState = clkA | clkB
(* types sent on the clerk's send and receive channels are argument types
of the memory and the RPC, respectively *)
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports Memory RPC MemClerk
begin
-datatype_new histState = histA | histB
+datatype histState = histA | histB
type_synonym histType = "(PrIds => histState) stfun" (* the type of the history variable *)
--- a/src/HOL/TLA/Memory/MemoryParameters.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
begin
(* the memory operations *)
-datatype_new memOp = read Locs | "write" Locs Vals
+datatype memOp = read Locs | "write" Locs Vals
consts
(* memory locations and contents *)
--- a/src/HOL/TLA/Memory/RPCParameters.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/TLA/Memory/RPCParameters.thy Thu Sep 11 19:32:36 2014 +0200
@@ -13,8 +13,8 @@
memory implementation.
*)
-datatype_new rpcOp = memcall memOp | othercall Vals
-datatype_new rpcState = rpcA | rpcB
+datatype rpcOp = memcall memOp | othercall Vals
+datatype rpcState = rpcA | rpcB
consts
(* some particular return values *)
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Sep 11 19:32:36 2014 +0200
@@ -341,7 +341,7 @@
fun not_co_datatype (T as Type (s, _)) =
if fp = Least_FP andalso
is_some (Old_Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then
- error (qsoty T ^ " is not a new-style datatype (cf. \"datatype_new\")")
+ error (qsoty T ^ " is not a new-style datatype (cf. \"datatype\")")
else
not_co_datatype0 T
| not_co_datatype T = not_co_datatype0 T;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 11 19:32:36 2014 +0200
@@ -1818,7 +1818,7 @@
(parse_co_datatype_cmd Least_FP construct_lfp);
val _ =
- Outer_Syntax.local_theory @{command_spec "datatype_new"} "define inductive datatypes"
+ Outer_Syntax.local_theory @{command_spec "datatype"} "define inductive datatypes"
(parse_co_datatype_cmd Least_FP construct_lfp);
val _ = Theory.setup (fp_antiquote_setup @{binding datatype});
--- a/src/HOL/Typerep.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Typerep.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
imports String
begin
-datatype_new typerep = Typerep String.literal "typerep list"
+datatype typerep = Typerep String.literal "typerep list"
class typerep =
fixes typerep :: "'a itself \<Rightarrow> typerep"
--- a/src/HOL/UNITY/Comp/Counter.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/UNITY/Comp/Counter.thy Thu Sep 11 19:32:36 2014 +0200
@@ -13,7 +13,7 @@
theory Counter imports "../UNITY_Main" begin
(* Variables are names *)
-datatype_new name = C | c nat
+datatype name = C | c nat
type_synonym state = "name=>int"
primrec sum :: "[nat,state]=>int" where
--- a/src/HOL/UNITY/Simple/Network.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/UNITY/Simple/Network.thy Thu Sep 11 19:32:36 2014 +0200
@@ -11,9 +11,9 @@
(*The state assigns a number to each process variable*)
-datatype_new pvar = Sent | Rcvd | Idle
+datatype pvar = Sent | Rcvd | Idle
-datatype_new pname = Aproc | Bproc
+datatype pname = Aproc | Bproc
type_synonym state = "pname * pvar => nat"
--- a/src/HOL/UNITY/Simple/Token.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/UNITY/Simple/Token.thy Thu Sep 11 19:32:36 2014 +0200
@@ -15,7 +15,7 @@
subsection{*Definitions*}
-datatype_new pstate = Hungry | Eating | Thinking
+datatype pstate = Hungry | Eating | Thinking
--{*process states*}
record state =
--- a/src/HOL/Unix/Nested_Environment.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Unix/Nested_Environment.thy Thu Sep 11 19:32:36 2014 +0200
@@ -19,7 +19,7 @@
position within the structure.
*}
-datatype_new (dead 'a, dead 'b, dead 'c) env =
+datatype (dead 'a, dead 'b, dead 'c) env =
Val 'a
| Env 'b "'c \<Rightarrow> ('a, 'b, 'c) env option"
--- a/src/HOL/Unix/Unix.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Unix/Unix.thy Thu Sep 11 19:32:36 2014 +0200
@@ -73,7 +73,7 @@
\cite{Naraschewski:2001}.}
*}
-datatype_new perm =
+datatype perm =
Readable
| Writable
| Executable -- "(ignored)"
@@ -284,7 +284,7 @@
@{text "root \<midarrow>x\<rightarrow> root'"} for the operational semantics.
*}
-datatype_new operation =
+datatype operation =
Read uid string path
| Write uid string path
| Chmod uid perms path
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy Thu Sep 11 19:32:36 2014 +0200
@@ -19,7 +19,7 @@
subsection {* Plain Ad Hoc Overloading *}
text {*Consider the type of first-order terms.*}
-datatype_new ('a, 'b) "term" =
+datatype ('a, 'b) "term" =
Var 'b |
Fun 'a "('a, 'b) term list"
--- a/src/HOL/ex/BT.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/BT.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
theory BT imports Main begin
-datatype_new 'a bt =
+datatype 'a bt =
Lf
| Br 'a "'a bt" "'a bt"
--- a/src/HOL/ex/Chinese.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Chinese.thy Thu Sep 11 19:32:36 2014 +0200
@@ -16,7 +16,7 @@
*}
-datatype_new shuzi =
+datatype shuzi =
One ("一")
| Two ("二")
| Three ("三")
--- a/src/HOL/ex/Eval_Examples.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Eval_Examples.thy Thu Sep 11 19:32:36 2014 +0200
@@ -42,7 +42,7 @@
text {* a fancy datatype *}
-datatype_new ('a, 'b) foo =
+datatype ('a, 'b) foo =
Foo "'a\<Colon>order" 'b
| Bla "('a, 'b) bar"
| Dummy nat
--- a/src/HOL/ex/Fundefs.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Fundefs.thy Thu Sep 11 19:32:36 2014 +0200
@@ -372,7 +372,7 @@
(* Simple Higher-Order Recursion *)
-datatype_new 'a tree =
+datatype 'a tree =
Leaf 'a
| Branch "'a tree list"
@@ -423,7 +423,7 @@
(* Many equations (quadratic blowup) *)
-datatype_new DT =
+datatype DT =
A | B | C | D | E | F | G | H | I | J | K | L | M | N | P
| Q | R | S | T | U | V
--- a/src/HOL/ex/Hebrew.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Hebrew.thy Thu Sep 11 19:32:36 2014 +0200
@@ -12,7 +12,7 @@
text {* The Hebrew Alef-Bet (א-ב). *}
-datatype_new alef_bet =
+datatype alef_bet =
Alef ("א")
| Bet ("ב")
| Gimel ("ג")
--- a/src/HOL/ex/Normalization_by_Evaluation.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy Thu Sep 11 19:32:36 2014 +0200
@@ -15,7 +15,7 @@
lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
lemma "~((0::nat) < (0::nat))" by normalization
-datatype_new n = Z | S n
+datatype n = Z | S n
primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where
"add Z = id"
--- a/src/HOL/ex/Records.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Records.thy Thu Sep 11 19:32:36 2014 +0200
@@ -166,7 +166,7 @@
subsection {* Coloured points: record extension *}
-datatype_new colour = Red | Green | Blue
+datatype colour = Red | Green | Blue
record cpoint = point +
colour :: colour
--- a/src/HOL/ex/Reflection_Examples.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Reflection_Examples.thy Thu Sep 11 19:32:36 2014 +0200
@@ -46,7 +46,7 @@
text {* Example 1 : Propositional formulae and NNF. *}
text {* The type @{text fm} represents simple propositional formulae: *}
-datatype_new form = TrueF | FalseF | Less nat nat
+datatype form = TrueF | FalseF | Less nat nat
| And form form | Or form form | Neg form | ExQ form
primrec interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool"
@@ -66,7 +66,7 @@
apply reify
oops
-datatype_new fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
+datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
where
@@ -135,7 +135,7 @@
text {* Example 2: Simple arithmetic formulae *}
text {* The type @{text num} reflects linear expressions over natural number *}
-datatype_new num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
+datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
text {* This is just technical to make recursive definitions easier. *}
primrec num_size :: "num \<Rightarrow> nat"
@@ -252,7 +252,7 @@
text {* Let's lift this to formulae and see what happens *}
-datatype_new aform = Lt num num | Eq num num | Ge num num | NEq num num |
+datatype aform = Lt num num | Eq num num | Ge num num | NEq num num |
Conj aform aform | Disj aform aform | NEG aform | T | F
primrec linaformsize:: "aform \<Rightarrow> nat"
@@ -331,7 +331,7 @@
one envornement of different types and show that automatic reification also deals with
bindings *}
-datatype_new rb = BC bool | BAnd rb rb | BOr rb rb
+datatype rb = BC bool | BAnd rb rb | BOr rb rb
primrec Irb :: "rb \<Rightarrow> bool"
where
@@ -343,7 +343,7 @@
apply (reify Irb.simps)
oops
-datatype_new rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
+datatype rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
| INeg rint | ISub rint rint
primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
@@ -370,7 +370,7 @@
apply (reify Irint_simps ("(3::int) * x + y * y - 9 + (- z)"))
oops
-datatype_new rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
+datatype rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> int list"
where
@@ -387,7 +387,7 @@
apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs"))
oops
-datatype_new rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
+datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
| NNeg rnat | NSub rnat rnat | Nlgth rlist
primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> nat list \<Rightarrow> nat"
@@ -418,7 +418,7 @@
("Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs)"))
oops
-datatype_new rifm = RT | RF | RVar nat
+datatype rifm = RT | RF | RVar nat
| RNLT rnat rnat | RNILT rnat rint | RNEQ rnat rnat
| RAnd rifm rifm | ROr rifm rifm | RImp rifm rifm| RIff rifm rifm
| RNEX rifm | RIEX rifm | RLEX rifm | RNALL rifm | RIALL rifm | RLALL rifm
@@ -451,7 +451,7 @@
text {* An example for equations containing type variables *}
-datatype_new prod = Zero | One | Var nat | Mul prod prod
+datatype prod = Zero | One | Var nat | Mul prod prod
| Pw prod nat | PNM nat nat prod
primrec Iprod :: " prod \<Rightarrow> ('a::linordered_idom) list \<Rightarrow>'a"
@@ -463,7 +463,7 @@
| "Iprod (Pw a n) vs = Iprod a vs ^ n"
| "Iprod (PNM n k t) vs = (vs ! n) ^ k * Iprod t vs"
-datatype_new sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F
+datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F
| Or sgn sgn | And sgn sgn
primrec Isgn :: "sgn \<Rightarrow> ('a::linordered_idom) list \<Rightarrow> bool"
--- a/src/HOL/ex/Refute_Examples.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Thu Sep 11 19:32:36 2014 +0200
@@ -605,7 +605,7 @@
text {* Non-recursive datatypes *}
-datatype_new T1 = A | B
+datatype T1 = A | B
lemma "P (x::T1)"
refute [expect = genuine]
@@ -639,7 +639,7 @@
refute [expect = genuine]
oops
-datatype_new 'a T2 = C T1 | D 'a
+datatype 'a T2 = C T1 | D 'a
lemma "P (x::'a T2)"
refute [expect = genuine]
@@ -669,7 +669,7 @@
refute [expect = genuine]
oops
-datatype_new ('a,'b) T3 = E "'a \<Rightarrow> 'b"
+datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
lemma "P (x::('a,'b) T3)"
refute [expect = genuine]
@@ -772,7 +772,7 @@
refute [expect = potential]
oops
-datatype_new BitList = BitListNil | Bit0 BitList | Bit1 BitList
+datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
lemma "P (x::BitList)"
refute [expect = potential]
--- a/src/HOL/ex/Seq.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Seq.thy Thu Sep 11 19:32:36 2014 +0200
@@ -8,7 +8,7 @@
imports Main
begin
-datatype_new 'a seq = Empty | Seq 'a "'a seq"
+datatype 'a seq = Empty | Seq 'a "'a seq"
fun conc :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq"
where
--- a/src/HOL/ex/Serbian.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Serbian.thy Thu Sep 11 19:32:36 2014 +0200
@@ -11,7 +11,7 @@
begin
text{* Serbian cyrillic letters *}
-datatype_new azbuka =
+datatype azbuka =
azbA ("А")
| azbB ("Б")
| azbV ("В")
@@ -47,7 +47,7 @@
thm azbuka.induct
text{* Serbian latin letters *}
-datatype_new abeceda =
+datatype abeceda =
abcA ("A")
| abcB ("B")
| abcC ("C")
--- a/src/HOL/ex/Sudoku.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Sudoku.thy Thu Sep 11 19:32:36 2014 +0200
@@ -19,7 +19,7 @@
no_notation Groups.one_class.one ("1")
-datatype_new digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
+datatype digit = A ("1") | B ("2") | C ("3") | D ("4") | E ("5") | F ("6") | G ("7") | H ("8") | I ("9")
definition valid :: "digit => digit => digit => digit => digit => digit => digit => digit => digit => bool" where
--- a/src/HOL/ex/Termination.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Termination.thy Thu Sep 11 19:32:36 2014 +0200
@@ -118,7 +118,7 @@
subsection {* Simple examples with other datatypes than nat, e.g. trees and lists *}
-datatype_new tree = Node | Branch tree tree
+datatype tree = Node | Branch tree tree
fun g_tree :: "tree * tree \<Rightarrow> tree"
where
--- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy Thu Sep 11 19:32:36 2014 +0200
@@ -6,7 +6,7 @@
imports "~~/src/HOL/Library/Transitive_Closure_Table"
begin
-datatype_new ty = A | B | C
+datatype ty = A | B | C
inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
where
--- a/src/HOL/ex/Tree23.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Tree23.thy Thu Sep 11 19:32:36 2014 +0200
@@ -21,16 +21,16 @@
type_synonym key = int -- {*for simplicity, should be a type class*}
-datatype_new ord = LESS | EQUAL | GREATER
+datatype ord = LESS | EQUAL | GREATER
definition "ord i j = (if i<j then LESS else if i=j then EQUAL else GREATER)"
-datatype_new 'a tree23 =
+datatype 'a tree23 =
Empty |
Branch2 "'a tree23" "key * 'a" "'a tree23" |
Branch3 "'a tree23" "key * 'a" "'a tree23" "key * 'a" "'a tree23"
-datatype_new 'a growth =
+datatype 'a growth =
Stay "'a tree23" |
Sprout "'a tree23" "key * 'a" "'a tree23"
@@ -402,7 +402,7 @@
text{* This is a little test harness and should be commented out once the
above functions have been proved correct. *}
-datatype_new 'a act = Add int 'a | Del int
+datatype 'a act = Add int 'a | Del int
fun exec where
"exec [] t = t" |
--- a/src/HOL/ex/Unification.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Unification.thy Thu Sep 11 19:32:36 2014 +0200
@@ -32,7 +32,7 @@
text {* Binary trees with leaves that are constants or variables. *}
-datatype_new 'a trm =
+datatype 'a trm =
Var 'a
| Const 'a
| Comb "'a trm" "'a trm" (infix "\<cdot>" 60)