# HG changeset patch # User blanchet # Date 1410456756 -7200 # Node ID 91ea607a34d8c7e95fba9cde7d1ea04af8639b51 # Parent a09ec6daaa19e6875386a02f5d1cfb2c228f66c2 updated news diff -r a09ec6daaa19 -r 91ea607a34d8 NEWS --- 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. diff -r a09ec6daaa19 -r 91ea607a34d8 src/Doc/Codegen/Evaluation.thy --- 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 \ 'a::order list \ 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/Doc/Codegen/Introduction.thy --- 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 [] []" diff -r a09ec6daaa19 -r 91ea607a34d8 src/Doc/Codegen/Refinement.thy --- 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 []" diff -r a09ec6daaa19 -r 91ea607a34d8 src/Doc/Datatypes/Datatypes.thy --- 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 \ 'a" text {* @@ -294,8 +294,8 @@ datatypes defined in terms of~@{text "\"}: *} - datatype_new ('a, 'b) fun_copy = Fun "'a \ 'b" - datatype_new 'a also_wrong = W1 | W2 (*<*)'a + datatype ('a, 'b) fun_copy = Fun "'a \ '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 \ 'a ftree" + datatype 'a ftree = FTLeaf 'a | FTNode "'a \ '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 \ local_theory"} + @{command_def "datatype"} & : & @{text "local_theory \ local_theory"} \end{matharray} @{rail \ - @@{command datatype_new} target? @{syntax dt_options}? \ + @@{command datatype} target? @{syntax dt_options}? \ (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \ @{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 \ nat list \ '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 \ 'a \ 'a ftree2" + datatype 'a ftree2 = FTLeaf2 'a | FTNode2 "'a \ 'a \ '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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/Doc/Datatypes/document/root.tex --- 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} diff -r a09ec6daaa19 -r 91ea607a34d8 src/Doc/Functions/Functions.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/Doc/Isar_Ref/Generic.thy --- 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. diff -r a09ec6daaa19 -r 91ea607a34d8 src/Doc/Isar_Ref/HOL_Specific.thy --- 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 \ 'a tree" +datatype 'a tree = Atom 'a | Branch "nat \ 'a tree" primrec map_tree :: "('a \ 'b) \ 'a tree \ '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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/Doc/Isar_Ref/Synopsis.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Auth/Event.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Auth/Message.thy --- 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*} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Auth/Public.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Auth/Smartcard/EventSC.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Auth/TLS.thy --- 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*) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/BNF_Least_Fixpoint.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Bali/AxSem.thy --- 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 @@ \prg=G,cls=C,lcl=L\\dom (locals (store s))\t\A ) \ s\\(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 = \'a. triple ('a assn) term ('a assn) **) ("{(1_)}/ _>/ {(1_)}" [3,65,3]75) type_synonym 'a triples = "'a triple set" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Bali/Basis.thy --- 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 \ '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 \ 'a" where "the_In1 (In1 a) = a" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Bali/Decl.thy --- 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 \ memberid" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Bali/Example.thy --- 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' \ tnam" and diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Bali/Name.thy --- 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 \ 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Bali/State.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Bali/Term.thy --- 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) "\name::mname,parTs::ty list,\::'a\" --{* 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 *} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Bali/Type.thy --- 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 *} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Bali/Value.thy --- 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 *} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Code_Evaluation.thy --- 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 \ typerep \ term" where "Const _ _ = dummy_term" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Codegenerator_Test/Code_Test.thy --- 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) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Datatype_Examples/Compat.thy --- 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 \ get_descrs @{theory} (1, 1, 1) @{type_name old_lst}; \ -datatype_new 'a lst = Nl | Cns 'a "'a lst" +datatype 'a lst = Nl | Cns 'a "'a lst" ML \ get_descrs @{theory} (0, 1, 1) @{type_name lst}; \ @@ -39,7 +39,7 @@ ML \ get_descrs @{theory} (1, 1, 1) @{type_name lst}; \ -datatype_new 'b w = W | W' "'b w \ 'b list" +datatype 'b w = W | W' "'b w \ 'b list" (* no support for sums of products: datatype_compat w @@ -47,11 +47,11 @@ ML \ get_descrs @{theory} (0, 1, 1) @{type_name w}; \ -datatype_new ('c, 'b) s = L 'c | R 'b +datatype ('c, 'b) s = L 'c | R 'b ML \ get_descrs @{theory} (0, 1, 1) @{type_name s}; \ -datatype_new 'd x = X | X' "('d x lst, 'd list) s" +datatype 'd x = X | X' "('d x lst, 'd list) s" ML \ get_descrs @{theory} (0, 1, 1) @{type_name x}; \ @@ -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 \ get_descrs @{theory} (0, 1, 1) @{type_name tttre}; \ @@ -78,7 +78,7 @@ thm tttre.induct tttre.rec thm compat_tttre.induct compat_tttre.rec -datatype_new 'a ftre = FEmp | FTre "'a \ 'a ftre lst" +datatype 'a ftre = FEmp | FTre "'a \ 'a ftre lst" ML \ get_descrs @{theory} (0, 1, 1) @{type_name ftre}; \ @@ -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 \ get_descrs @{theory} (0, 1, 1) @{type_name btre}; \ @@ -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 \ get_descrs @{theory} (0, 2, 2) @{type_name foo}; \ ML \ get_descrs @{theory} (0, 2, 2) @{type_name bar}; \ @@ -110,7 +110,7 @@ ML \ get_descrs @{theory} (2, 2, 2) @{type_name foo}; \ ML \ get_descrs @{theory} (2, 2, 2) @{type_name bar}; \ -datatype_new 'a tre = Tre 'a "'a tre lst" +datatype 'a tre = Tre 'a "'a tre lst" ML \ get_descrs @{theory} (0, 1, 1) @{type_name tre}; \ @@ -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 \ get_descrs @{theory} (0, 2, 2) @{type_name f}; \ ML \ get_descrs @{theory} (0, 2, 2) @{type_name g}; \ -datatype_new h = H "h f" | H' +datatype h = H "h f" | H' ML \ get_descrs @{theory} (0, 1, 1) @{type_name h}; \ @@ -143,7 +143,7 @@ thm h.induct h.rec thm compat_h.induct compat_h.rec -datatype_new myunit = MyUnity +datatype myunit = MyUnity ML \ get_descrs @{theory} (0, 1, 1) @{type_name myunit}; \ @@ -151,7 +151,7 @@ ML \ get_descrs @{theory} (1, 1, 1) @{type_name myunit}; \ -datatype_new mylist = MyNil | MyCons nat mylist +datatype mylist = MyNil | MyCons nat mylist ML \ get_descrs @{theory} (0, 1, 1) @{type_name mylist}; \ @@ -159,7 +159,7 @@ ML \ get_descrs @{theory} (1, 1, 1) @{type_name mylist}; \ -datatype_new foo' = FooNil | FooCons bar' foo' and bar' = Bar +datatype foo' = FooNil | FooCons bar' foo' and bar' = Bar ML \ get_descrs @{theory} (0, 2, 2) @{type_name foo'}; \ ML \ get_descrs @{theory} (0, 2, 2) @{type_name bar'}; \ @@ -177,7 +177,7 @@ ML \ get_descrs @{theory} (1, 1, 1) @{type_name fnky}; \ -datatype_new tree = Tree "tree foo" +datatype tree = Tree "tree foo" ML \ get_descrs @{theory} (0, 1, 1) @{type_name tree}; \ diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Datatype_Examples/IsaFoR_Datatypes.thy --- 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 \ nat) \ nat) list" +datatype (discs_sels) 'f projL = Projection "(('f \ nat) \ 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 ("\") | 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 ("\") | PCons "nat" "pos" (infixr "<#" 70) +datatype (discs_sels) pos = Empty ("\") | PCons "nat" "pos" (infixr "<#" 70) type_synonym ('f, 'v) prseq = "(pos \ ('f, 'v) rule \ bool \ ('f, 'v) term) list" type_synonym ('f, 'v) rseq = "(pos \ ('f, 'v) rule \ ('f, 'v) term) list" @@ -49,7 +49,7 @@ type_synonym ('f, 'l, 'v) qtrsLL = "bool \ ('f, 'l, 'v) termsLL \ ('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 \ ('f, 'v) term \ 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 \ nat) \ (nat \ 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 \ nat) \ af_entry) list" type_synonym 'f prec_weight_repr = "(('f \ nat) \ (nat \ nat \ (nat list option))) list \ 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 \ nat) \ (nat \ 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 \ nat) \ 'f list) list" type_synonym ('f, 'v) uncurry_info = "'f \ 'f sig_map_list \ ('f, 'v) rules \ ('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 \ nat) \ arithFun) list" -datatype_new (discs_sels) ('f, 'v) sl_variant = +datatype (discs_sels) 'f sl_inter = SL_Inter nat "(('f \ nat) \ arithFun) list" +datatype (discs_sels) ('f, 'v) sl_variant = Rootlab "('f \ nat) option" | Finitelab "'f sl_inter" | QuasiFinitelab "'f sl_inter" 'v type_synonym ('f, 'v) crit_pair_joins = "(('f, 'v) term \ ('f, 'v) rseq \ ('f, 'v) term \ ('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 \ ('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 \ ('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 \ (('f, 'v) term \ 'v list) list \ ('f, 'v) cond_constraint \ ('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 \ ('f, 'v) rules \ ('f, 'v) cond_constraint_prf) list" nat nat -datatype_new (discs_sels) ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \ _") -datatype_new (discs_sels) ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \ 'q) list" -datatype_new (discs_sels) 'q ta_relation = +datatype (discs_sels) ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \ _") +datatype (discs_sels) ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \ 'q) list" +datatype (discs_sels) 'q ta_relation = Decision_Proc | Id_Relation | Some_Relation "('q \ '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 \ 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 \ 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 \ ('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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Datatype_Examples/Lambda_Term.thy --- 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" | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Datatype_Examples/Misc_Datatype.thy --- 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 \ 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 \ 'a ftree" +datatype (discs_sels) 'a ftree = FTLeaf 'a | FTNode "'a \ 'a ftree" -datatype_new (discs_sels) ('a, 'b, 'c) some_killing = +datatype (discs_sels) ('a, 'b, 'c) some_killing = SK "'a \ 'b \ ('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 \ 'b \ 'b nofail2 \ 'b) list" -datatype_new (discs_sels) 'b nofail3 = NF3 'b "('b nofail3 \ 'b \ 'b nofail3 \ 'b) fset" -datatype_new (discs_sels) 'b nofail4 = NF4 "('b nofail4 \ ('b nofail4 \ 'b \ 'b nofail4 \ 'b) fset) list" +datatype (discs_sels) 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b +datatype (discs_sels) 'b nofail2 = NF2 "('b nofail2 \ 'b \ 'b nofail2 \ 'b) list" +datatype (discs_sels) 'b nofail3 = NF3 'b "('b nofail3 \ 'b \ 'b nofail3 \ 'b) fset" +datatype (discs_sels) 'b nofail4 = NF4 "('b nofail4 \ ('b nofail4 \ 'b \ 'b nofail4 \ '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 \ 'a" -datatype_new (discs_sels) 'a deadbar_option = DeadBarOption "'a option \ 'a option" -datatype_new (discs_sels) ('a, 'b) bar = Bar "'b \ 'a" -datatype_new (discs_sels) ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \ 'c + 'a" -datatype_new (discs_sels) 'a deadfoo = DeadFoo "'a \ 'a + 'a" +datatype (discs_sels) 'a deadbar = DeadBar "'a \ 'a" +datatype (discs_sels) 'a deadbar_option = DeadBarOption "'a option \ 'a option" +datatype (discs_sels) ('a, 'b) bar = Bar "'b \ 'a" +datatype (discs_sels) ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \ 'c + 'a" +datatype (discs_sels) 'a deadfoo = DeadFoo "'a \ '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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Datatype_Examples/Process.thy --- 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 \ char list process" where "xyax = x \ 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Datatype_Examples/Stream_Processor.thy --- 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>\ = Get "'a \ ('a, 'b, 'c) sp\<^sub>\" | Put "'b" "'c" +datatype ('a, 'b, 'c) sp\<^sub>\ = Get "'a \ ('a, 'b, 'c) sp\<^sub>\" | Put "'b" "'c" codatatype ('a, 'b) sp\<^sub>\ = In (out: "('a, 'b, ('a, 'b) sp\<^sub>\) sp\<^sub>\") primrec run\<^sub>\ :: "('a, 'b, 'c) sp\<^sub>\ \ 'a stream \ ('b \ 'c) \ 'a stream" where @@ -170,7 +170,7 @@ lemma \_assl: "F id assl o \ = \ o map_prod \ id o assl" unfolding assl_def \_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>\ = GetF "'a \ ('a, 'b, 'c) spF\<^sub>\" | PutF "('b,'c) F" +datatype ('a, 'b, 'c) spF\<^sub>\ = GetF "'a \ ('a, 'b, 'c) spF\<^sub>\" | PutF "('b,'c) F" codatatype ('a, 'b) spF\<^sub>\ = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\) spF\<^sub>\") codatatype 'b JF = Ctor (dtor: "('b, 'b JF) F") diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Decision_Procs/Approximation.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Decision_Procs/Commutative_Ring.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Decision_Procs/Cooper.thy --- 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 \ 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Decision_Procs/Ferrack.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Decision_Procs/MIR.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- 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 \ C (0\<^sub>N)" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Enum.thy --- 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") diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Extraction.thy --- 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 *} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/HOLCF/Discrete.thy --- 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 *} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/HOLCF/FOCUS/Buffer.thy --- 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 ("\") -datatype_new +datatype State = Sd D | Snil ("\") type_synonym diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/HOLCF/IOA/ABP/Abschannel.thy --- 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 (********************************************************** diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/HOLCF/IOA/ABP/Action.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/HOLCF/IOA/NTP/Abschannel.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/HOLCF/IOA/NTP/Action.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/HOLCF/IOA/Storage/Action.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/HOLCF/IOA/ex/TrivEx.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/HOLCF/IOA/ex/TrivEx2.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/HOLCF/Up.thy --- 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>\)" [1000] 999) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Hoare/Heap.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Hoare/Hoare_Logic.thy --- 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 \ 'a" | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Hoare/Hoare_Logic_Abort.thy --- 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 \ 'a" | Abort | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Hoare_Parallel/Graph.thy --- 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 \ nat" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Hoare_Parallel/OG_Com.thy --- 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 \ 'a)" | AnnSeq "('a ann_com)" "('a ann_com)" | AnnCond1 "('a assn)" "('a bexp)" "('a ann_com)" "('a ann_com)" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Hoare_Parallel/RG_Com.thy --- 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 \'a" | Seq "'a com" "'a com" | Cond "'a bexp" "'a com" "'a com" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/ACom.thy --- 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) | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/AExp.thy --- 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 \ 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}{% *} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/ASM.thy --- 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}{% *} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Abs_Int1_const.thy --- 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 \_const where "\_const (Const i) = {i}" | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Abs_Int1_parity.thy --- 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}: *} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy --- 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}" | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy --- 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 < diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy --- 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"\"}: *} -datatype_new 'a astate = FunDom "string \ 'a" "string list" +datatype 'a astate = FunDom "string \ 'a" "string list" fun "fun" where "fun (FunDom f _) = f" fun dom where "dom (FunDom _ A) = A" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy --- 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) | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy --- 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 \_const where "\_const (Const n) = {n}" | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy --- 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}: *} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy --- 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 "\_ivl i = (case i of I (Some l) (Some h) \ {l..h} | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy --- 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"\"}: *} -datatype_new 'a st = FunDom "vname \ 'a" "vname list" +datatype 'a st = FunDom "vname \ 'a" "vname list" fun "fun" where "fun (FunDom f xs) = f" fun dom where "dom (FunDom f xs) = xs" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/BExp.thy --- 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 \ state \ bool" where diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/C_like.thy --- 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 \ nat" -datatype_new aexp = N nat | Deref aexp ("!") | Plus aexp aexp +datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp fun aval :: "aexp \ state \ 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 \ state \ 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Com.thy --- 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) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Compiler.thy --- 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*} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/OO.thy --- 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 \ ref" type_synonym venv = "string \ ref" type_synonym store = "addr \ obj" -datatype_new exp = +datatype exp = Null | New | V string | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Poly_Types.thy --- 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. *} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Procs.thy --- 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) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/Types.thy --- 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 \ 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 \ state \ val \ 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 \ state \ bool \ 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 \ ty" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMP/VCG.thy --- 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) | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMPP/Com.thy --- 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) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMPP/Hoare.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 \ ('a \ heap) option" +datatype 'a Heap = Heap "heap \ ('a \ heap) option" lemma [code, code del]: "(Code_Evaluation.term_of :: 'a::typerep Heap \ Code_Evaluation.term) = Code_Evaluation.term_of" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Imperative_HOL/ex/SatChecker.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Induct/ABexp.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Induct/Com.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Induct/Comb.thy --- 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) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Induct/Common_Patterns.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Induct/Ordinals.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Induct/PropLog.thy --- 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) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Induct/QuoDataType.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Induct/QuoNestedDataType.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Induct/Term.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Induct/Tree.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Isar_Examples/Expr_Compiler.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Isar_Examples/Hoare.thy --- 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 \ 'a" | Seq "'a com" "'a com" ("(_;/ _)" [60, 61] 60) | Cond "'a bexp" "'a com" "'a com" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Isar_Examples/Nested_Datatype.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Lattice/Orders.thy --- 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 \ 'a" where undual_dual: "undual (dual x) = x" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Lazy_Sequence.thy --- 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 \ 'a list" where diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Library/Extended.thy --- 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 ("\") | Minf ("-\") +datatype 'a extended = Fin 'a | Pinf ("\") | Minf ("-\") instantiation extended :: (order)order diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Library/Extended_Real.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Library/IArray.thy --- 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 \ 'a list" where "list_of (IArray xs) = xs" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Library/Lattice_Constructions.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Library/Parallel.thy --- 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 \ 'a" +datatype 'a future = fork "unit \ 'a" primrec join :: "'a future \ 'a" where "join (fork f) = f ()" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Library/Phantom_Type.thy --- 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 \ 'b" where "of_phantom (phantom x) = x" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Library/RBT_Impl.thy --- 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 \ l | _ \ t')" -datatype_new compare = LT | GT | EQ +datatype compare = LT | GT | EQ partial_function (tailrec) compare_height :: "('a, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt \ compare" where diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Library/Tree.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/List.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Metis_Examples/Binary_Tree.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Metis_Examples/Message.thy --- 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*} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Metis_Examples/Trans_Closure.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/MicroJava/DFA/Err.thy --- 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 \ 'a \ 'a err" type_synonym 'a esl = "'a set * 'a ord * 'a ebinop" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/MicroJava/J/Example.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/MicroJava/J/Term.thy --- 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) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/MicroJava/J/Type.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/MicroJava/J/Value.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/MicroJava/JVM/JVMDefensive.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/MicroJava/JVM/JVMInstructions.thy --- 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)" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/NanoJava/Decl.thy --- 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 *} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/NanoJava/State.thy --- 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 *} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/NanoJava/Term.thy --- 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 \ 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) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Nitpick.thy --- 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 \ '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 \ 'b" +datatype (dead 'a, dead 'b) pair_box = PairBox 'a 'b +datatype (dead 'a) word = Word "'a set" typedecl bisim_iterator typedecl unsigned_bit diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Nitpick_Examples/Datatype_Nits.thy --- 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 \ 'b" +datatype ('a, 'b) pd = Pd "'a \ 'b" fun fs where "fs (Pd (a, _)) = a" @@ -76,7 +76,7 @@ nitpick [expect = genuine] oops -datatype_new ('a, 'b) fn = Fn "'a \ 'b" +datatype ('a, 'b) fn = Fn "'a \ 'b" fun app where "app (Fn f) x = f x" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Nitpick_Examples/Integer_Nits.thy --- 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 = {}" | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Nitpick_Examples/Manual_Nits.thy --- 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 "[] \ S\<^sub>1" @@ -381,7 +381,7 @@ subsection {* 3.2. AA Trees *} -datatype_new 'a aa_tree = \ | N "'a\linorder" nat "'a aa_tree" "'a aa_tree" +datatype 'a aa_tree = \ | N "'a\linorder" nat "'a aa_tree" "'a aa_tree" primrec data where "data \ = undefined" | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Nitpick_Examples/Refute_Nits.thy --- 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\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\'a T2)" nitpick [expect = genuine] @@ -685,7 +685,7 @@ nitpick [expect = genuine] oops -datatype_new ('a, 'b) T3 = E "'a \ 'b" +datatype ('a, 'b) T3 = E "'a \ 'b" lemma "P (x\('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\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\'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\'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\X)" nitpick [expect = genuine] @@ -999,7 +999,7 @@ text {* Indirect recursion is implemented via mutual recursion. *} -datatype_new XOpt = CX "XOpt option" | DX "bool \ XOpt option" +datatype XOpt = CX "XOpt option" | DX "bool \ XOpt option" lemma "P (x\XOpt)" nitpick [expect = genuine] @@ -1017,7 +1017,7 @@ nitpick [expect = genuine] oops -datatype_new 'a YOpt = CY "('a \ 'a YOpt) option" +datatype 'a YOpt = CY "('a \ 'a YOpt) option" lemma "P (x\'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\Trie)" nitpick [expect = genuine] @@ -1045,7 +1045,7 @@ nitpick [expect = genuine] oops -datatype_new InfTree = Leaf | Node "nat \ InfTree" +datatype InfTree = Leaf | Node "nat \ InfTree" lemma "P (x\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 \ 'a lambda" +datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \ 'a lambda" lemma "P (x\'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 \ bool" | D "'b list" -datatype_new 'c U = E "('c, 'c U) T" +datatype (dead 'a, 'b) T = C "'a \ bool" | D "'b list" +datatype 'c U = E "('c, 'c U) T" lemma "P (x\'c U)" nitpick [expect = genuine] diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Nominal/Examples/CK_Machine.thy --- 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 ("\") | CAPPL "ctx" "lam" | CAPPR "lam" "ctx" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Nominal/Examples/Pattern.thy --- 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 "\x:T. t \ Abs T x t" -datatype_new pat = +datatype pat = PVar name ty | PTuple pat pat ("(1'\\_,/ _'\\)") diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Nominal/Nominal.thy --- 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 \ 'x) \ 'x \ '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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Num.thy --- 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} *} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Option.thy --- 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) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate.thy --- 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 \ bool" +datatype 'a pred = Pred "'a \ bool" primrec eval :: "'a pred \ 'a \ 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 \ 'a pred" where "pred_of_seq Empty = \" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy --- 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 "[] \ S\<^sub>1" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/Examples.thy --- 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 "[] \ 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 "\" 200) -datatype_new dB = +datatype dB = Var nat | App dB dB (infixl "\" 200) | Abs type dB @@ -237,12 +237,12 @@ type_synonym vvalue = int type_synonym var_assign = "vname \ 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 \ nat" -datatype_new aexp = N nat | V name | Plus aexp aexp +datatype aexp = N nat | V name | Plus aexp aexp fun aval :: "aexp \ state' \ 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 \ state' \ bool" where "bval (B b) _ = b" | @@ -282,7 +282,7 @@ "bval (And b1 b2) st = (bval b1 st \ 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 \ nat \ proc \ bool" where "step (pre n p) n p" | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/Hotel_Example.thy --- 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 \ key" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/IMP_1.thy --- 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 | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/IMP_2.thy --- 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 | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/IMP_3.thy --- 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 | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/IMP_4.thy --- 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 | diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/Lambda_Example.thy --- 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 "\" 200) -datatype_new dB = +datatype dB = Var nat | App dB dB (infixl "\" 200) | Abs type dB diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy --- 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 "[] \ 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 "\" 200) -datatype_new dB = +datatype dB = Var nat | App dB dB (infixl "\" 200) | Abs type dB diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy --- 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 \ nat \ proc) \ 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 \ 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy --- 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 \ Nat \ Nat" @@ -20,10 +20,10 @@ Zer \ Zer | Suc x' \ 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy --- 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\fst x\\<^sub>? = \ \ unique xs)" -datatype_new type = +datatype type = TVar nat | Top | Fun type type (infixr "\" 200) | TyAll type type ("(3\<:_./ _)" [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 \ 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\:_./ _)" [0, 10] 10) | TAbs type trm ("(3\<:_./ _)" [0, 10] 10) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Proofs/Extraction/Higman.thy --- 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 \ letter list \ bool" where diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Proofs/Extraction/Warshall.thy --- 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 \ 'a \ b) \ 'a \ 'a list \ 'a \ bool" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Proofs/Lambda/Lambda.thy --- 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 "\" 200) | Abs dB diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Proofs/Lambda/LambdaType.thy --- 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 "\" 200) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy --- 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) \ (Key ` pubEK ` agents)" -datatype_new +datatype event = Says agent agent msg | Gets agent msg | Notes agent msg diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Quickcheck_Examples/Hotel_Example.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy --- 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 \ '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 \ '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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy --- 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 \ 'a set" where diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Quickcheck_Exhaustive.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Quickcheck_Narrowing.thy --- 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 \ '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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Quotient_Examples/Quotient_Message.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Record.thy --- 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 \ 'b \ 'c" "'b \ 'c \ 'a" primrec diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/SET_Protocol/Event_SET.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/SET_Protocol/Message_SET.thy --- 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*} diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/SPARK/Manual/Complex_Types.thy --- 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 \ day \ int" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Statespace/DistinctTreeProver.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/String.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/TLA/Inc/Inc.thy --- 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 *) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/TLA/Memory/MemClerkParameters.thy --- 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 *) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/TLA/Memory/MemoryImplementation.thy --- 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 *) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/TLA/Memory/MemoryParameters.thy --- 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 *) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/TLA/Memory/RPCParameters.thy --- 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 *) diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- 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; diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Tools/BNF/bnf_lfp.ML --- 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}); diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Typerep.thy --- 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 \ typerep" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/UNITY/Comp/Counter.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/UNITY/Simple/Network.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/UNITY/Simple/Token.thy --- 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 = diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Unix/Nested_Environment.thy --- 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 \ ('a, 'b, 'c) env option" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Unix/Unix.thy --- 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 \x\ root'"} for the operational semantics. *} -datatype_new operation = +datatype operation = Read uid string path | Write uid string path | Chmod uid perms path diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Adhoc_Overloading_Examples.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/BT.thy --- 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" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Chinese.thy --- 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 ("三") diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Eval_Examples.thy --- 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\order" 'b | Bla "('a, 'b) bar" | Dummy nat diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Fundefs.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Hebrew.thy --- 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 ("ג") diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Normalization_by_Evaluation.thy --- 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 \ n \ n" where "add Z = id" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Records.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Reflection_Examples.thy --- 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 \ ('a::ord) list \ 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 \ bool list \ 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 \ 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 \ 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 \ 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 \ int list \ 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 \ int list \ int list list \ 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 \ int list \ int list list \ nat list \ 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 \ ('a::linordered_idom) list \'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 \ ('a::linordered_idom) list \ bool" diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Refute_Examples.thy --- 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 \ 'b" +datatype ('a,'b) T3 = E "'a \ '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] diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Seq.thy --- 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 \ 'a seq \ 'a seq" where diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Serbian.thy --- 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") diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Sudoku.thy --- 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 diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Termination.thy --- 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 \ tree" where diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Transitive_Closure_Table_Ex.thy --- 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 \ ty \ bool" where diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Tree23.thy --- 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" 60)