--- a/src/HOL/Auth/Message.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Auth/Message.thy Tue Sep 09 20:51:36 2014 +0200
@@ -35,10 +35,10 @@
definition symKeys :: "key set" where
"symKeys == {K. invKey K = K}"
-datatype --{*We allow any number of friendly agents*}
+datatype_new --{*We allow any number of friendly agents*}
agent = Server | Friend nat | Spy
-datatype
+datatype_new
msg = Agent agent --{*Agent names*}
| Number nat --{*Ordinary integers, timestamps, ...*}
| Nonce nat --{*Unguessable nonces*}
--- a/src/HOL/Auth/Public.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Auth/Public.thy Tue Sep 09 20:51:36 2014 +0200
@@ -16,7 +16,7 @@
subsection{*Asymmetric Keys*}
-datatype keymode = Signature | Encryption
+datatype_new keymode = Signature | Encryption
consts
publicKey :: "[keymode,agent] => key"
--- a/src/HOL/Auth/Smartcard/EventSC.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Auth/Smartcard/EventSC.thy Tue Sep 09 20:51:36 2014 +0200
@@ -9,10 +9,10 @@
consts (*Initial states of agents -- parameter of the construction*)
initState :: "agent => msg set"
-datatype card = Card agent
+datatype_new card = Card agent
text{*Four new events express the traffic between an agent and his card*}
-datatype
+datatype_new
event = Says agent agent msg
| Notes agent msg
| Gets agent msg
--- a/src/HOL/Auth/TLS.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Auth/TLS.thy Tue Sep 09 20:51:36 2014 +0200
@@ -49,7 +49,7 @@
signature. Therefore, we formalize signature as encryption using the
private encryption key.*}
-datatype role = ClientRole | ServerRole
+datatype_new role = ClientRole | ServerRole
consts
(*Pseudo-random function of Section 5*)
--- a/src/HOL/BNF_Examples/Process.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/BNF_Examples/Process.thy Tue Sep 09 20:51:36 2014 +0200
@@ -79,7 +79,7 @@
subsection{* Multi-guard fixpoint definitions, simulated with auxiliary arguments *}
-datatype x_y_ax = x | y | ax
+datatype_new x_y_ax = x | y | ax
primcorec F :: "x_y_ax \<Rightarrow> char list process" where
"xyax = x \<Longrightarrow> isChoice (F xyax)"
@@ -106,7 +106,7 @@
hide_const x y ax X Y AX
(* Process terms *)
-datatype ('a,'pvar) process_term =
+datatype_new ('a,'pvar) process_term =
VAR 'pvar |
PROC "'a process" |
ACT 'a "('a,'pvar) process_term" | CH "('a,'pvar) process_term" "('a,'pvar) process_term"
--- a/src/HOL/Bali/AxSem.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Bali/AxSem.thy Tue Sep 09 20:51:36 2014 +0200
@@ -378,7 +378,7 @@
\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
\<and> s\<Colon>\<preceq>(G,L))"
-datatype 'a triple = triple "('a assn)" "term" "('a assn)" (** should be
+datatype_new 'a triple = triple "('a assn)" "term" "('a assn)" (** should be
something like triple = \<forall>'a. triple ('a assn) term ('a assn) **)
("{(1_)}/ _>/ {(1_)}" [3,65,3]75)
type_synonym 'a triples = "'a triple set"
--- a/src/HOL/Bali/Basis.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Bali/Basis.thy Tue Sep 09 20:51:36 2014 +0200
@@ -155,7 +155,7 @@
primrec the_Inr :: "'a + 'b \<Rightarrow> 'b"
where "the_Inr (Inr b) = b"
-datatype ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
+datatype_new ('a, 'b, 'c) sum3 = In1 'a | In2 'b | In3 'c
primrec the_In1 :: "('a, 'b, 'c) sum3 \<Rightarrow> 'a"
where "the_In1 (In1 a) = a"
--- a/src/HOL/Bali/Decl.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Bali/Decl.thy Tue Sep 09 20:51:36 2014 +0200
@@ -42,7 +42,7 @@
subsubsection {* Access modifier *}
-datatype acc_modi (* access modifier *)
+datatype_new 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 memberdecl = fdecl fdecl | mdecl mdecl
+datatype_new memberdecl = fdecl fdecl | mdecl mdecl
-datatype memberid = fid vname | mid sig
+datatype_new memberid = fid vname | mid sig
class has_memberid =
fixes memberid :: "'a \<Rightarrow> memberid"
--- a/src/HOL/Bali/Example.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Bali/Example.thy Tue Sep 09 20:51:36 2014 +0200
@@ -66,9 +66,9 @@
section "type and expression names"
(** unfortunately cannot simply instantiate tnam **)
-datatype tnam' = HasFoo' | Base' | Ext' | Main'
-datatype vnam' = arr' | vee' | z' | e'
-datatype label' = lab1'
+datatype_new tnam' = HasFoo' | Base' | Ext' | Main'
+datatype_new vnam' = arr' | vee' | z' | e'
+datatype_new label' = lab1'
axiomatization
tnam' :: "tnam' \<Rightarrow> tnam" and
--- a/src/HOL/Bali/Name.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Bali/Name.thy Tue Sep 09 20:51:36 2014 +0200
@@ -12,11 +12,11 @@
typedecl vname --{* variable or field name *}
typedecl label --{* label as destination of break or continue *}
-datatype ename --{* expression name *}
+datatype_new ename --{* expression name *}
= VNam vname
| Res --{* special name to model the return value of methods *}
-datatype lname --{* names for local variables and the This pointer *}
+datatype_new lname --{* names for local variables and the This pointer *}
= EName ename
| This
abbreviation VName :: "vname \<Rightarrow> lname"
@@ -25,7 +25,7 @@
abbreviation Result :: lname
where "Result == EName Res"
-datatype xname --{* names of standard exceptions *}
+datatype_new xname --{* names of standard exceptions *}
= Throwable
| NullPointer | OutOfMemory | ClassCast
| NegArrSize | IndOutBound | ArrStore
@@ -39,7 +39,7 @@
done
-datatype tname --{* type names for standard classes and other type names *}
+datatype_new tname --{* type names for standard classes and other type names *}
= Object'
| SXcpt' xname
| TName tnam
--- a/src/HOL/Bali/State.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Bali/State.thy Tue Sep 09 20:51:36 2014 +0200
@@ -19,7 +19,7 @@
section "objects"
-datatype obj_tag = --{* tag for generic object *}
+datatype_new 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 st = (* pure state, i.e. contents of all variables *)
+datatype_new st = (* pure state, i.e. contents of all variables *)
st globs locals
subsection "access"
--- a/src/HOL/Bali/Term.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Bali/Term.thy Tue Sep 09 20:51:36 2014 +0200
@@ -60,20 +60,20 @@
type_synonym locals = "(lname, val) table" --{* local variables *}
-datatype jump
+datatype_new jump
= Break label --{* break *}
| Cont label --{* continue *}
| Ret --{* return from method *}
-datatype xcpt --{* exception *}
+datatype_new xcpt --{* exception *}
= Loc loc --{* location of allocated execption object *}
| Std xname --{* intermediate standard exception, see Eval.thy *}
-datatype error
+datatype_new error
= AccessViolation --{* Access to a member that isn't permitted *}
| CrossMethodJump --{* Method exits with a break or continue *}
-datatype abrupt --{* abrupt completion *}
+datatype_new 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 inv_mode --{* invocation mode for method calls *}
+datatype_new inv_mode --{* invocation mode for method calls *}
= Static --{* static *}
| SuperM --{* super *}
| IntVir --{* interface or virtual *}
@@ -104,13 +104,13 @@
(type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
--{* function codes for unary operations *}
-datatype unop = UPlus -- {*{\tt +} unary plus*}
+datatype_new unop = UPlus -- {*{\tt +} unary plus*}
| UMinus -- {*{\tt -} unary minus*}
| UBitNot -- {*{\tt ~} bitwise NOT*}
| UNot -- {*{\tt !} logical complement*}
--{* function codes for binary operations *}
-datatype binop = Mul -- {*{\tt * } multiplication*}
+datatype_new 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 var
+datatype_new var
= LVar lname --{* local variable (incl. parameters) *}
| FVar qtname qtname bool expr vname ("{_,_,_}_.._"[10,10,10,85,99]90)
--{* class field *}
--- a/src/HOL/Bali/Type.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Bali/Type.thy Tue Sep 09 20:51:36 2014 +0200
@@ -14,13 +14,13 @@
\end{itemize}
*}
-datatype prim_ty --{* primitive type, cf. 4.2 *}
+datatype_new prim_ty --{* primitive type, cf. 4.2 *}
= Void --{* result type of void methods *}
| Boolean
| Integer
-datatype ref_ty --{* reference type, cf. 4.3 *}
+datatype_new ref_ty --{* reference type, cf. 4.3 *}
= NullT --{* null type, cf. 4.1 *}
| IfaceT qtname --{* interface type *}
| ClassT qtname --{* class type *}
--- a/src/HOL/Bali/Value.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Bali/Value.thy Tue Sep 09 20:51:36 2014 +0200
@@ -9,7 +9,7 @@
typedecl loc --{* locations, i.e. abstract references on objects *}
-datatype val
+datatype_new val
= Unit --{* dummy result value of void methods *}
| Bool bool --{* Boolean value *}
| Intg int --{* integer value *}
--- a/src/HOL/Codegenerator_Test/Code_Test.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test.thy Tue Sep 09 20:51:36 2014 +0200
@@ -11,7 +11,7 @@
subsection {* YXML encoding for @{typ Code_Evaluation.term} *}
-datatype yxml_of_term = YXML
+datatype_new 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 xml_tree = XML_Tree
+datatype_new xml_tree = XML_Tree
lemma xml_tree_anything: "x = (y :: xml_tree)"
by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)
--- a/src/HOL/Decision_Procs/Approximation.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Tue Sep 09 20:51:36 2014 +0200
@@ -2037,7 +2037,7 @@
subsection "Define syntax and semantics"
-datatype floatarith
+datatype_new floatarith
= Add floatarith floatarith
| Minus floatarith
| Mult floatarith floatarith
@@ -2456,7 +2456,7 @@
show ?case by (cases "n < length vs", auto)
qed
-datatype form = Bound floatarith floatarith floatarith form
+datatype_new form = Bound floatarith floatarith floatarith form
| Assign floatarith floatarith form
| Less floatarith floatarith
| LessEqual floatarith floatarith
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Tue Sep 09 20:51:36 2014 +0200
@@ -11,12 +11,12 @@
text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
-datatype 'a pol =
+datatype_new 'a pol =
Pc 'a
| Pinj nat "'a pol"
| PX "'a pol" nat "'a pol"
-datatype 'a polex =
+datatype_new 'a polex =
Pol "'a pol"
| Add "'a polex" "'a polex"
| Sub "'a polex" "'a polex"
--- a/src/HOL/Decision_Procs/Cooper.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Tue Sep 09 20:51:36 2014 +0200
@@ -15,7 +15,7 @@
(**** SHADOW SYNTAX AND SEMANTICS ****)
(*********************************************************************************)
-datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
+datatype_new num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
| Mul int num
primrec num_size :: "num \<Rightarrow> nat" -- {* A size for num to make inductive proofs simpler *}
@@ -38,7 +38,7 @@
| "Inum bs (Sub a b) = Inum bs a - Inum bs b"
| "Inum bs (Mul c a) = c* Inum bs a"
-datatype fm =
+datatype_new fm =
T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
| Closed nat | NClosed nat
--- a/src/HOL/Decision_Procs/Ferrack.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Tue Sep 09 20:51:36 2014 +0200
@@ -13,7 +13,7 @@
(**** SHADOW SYNTAX AND SEMANTICS ****)
(*********************************************************************************)
-datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
+datatype_new 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 fm =
+datatype_new fm =
T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num|
NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
--- a/src/HOL/Decision_Procs/MIR.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Tue Sep 09 20:51:36 2014 +0200
@@ -105,7 +105,7 @@
(**** SHADOW SYNTAX AND SEMANTICS ****)
(*********************************************************************************)
-datatype num = C int | Bound nat | CN nat int num | Neg num | Add num num| Sub num num
+datatype_new 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 fm =
+datatype_new fm =
T| F| Lt num| Le num| Gt num| Ge num| Eq num| NEq num| Dvd int num| NDvd int num|
NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 09 20:51:36 2014 +0200
@@ -15,7 +15,7 @@
subsection {* Terms *}
-datatype tm = CP poly | Bound nat | Add tm tm | Mul poly tm
+datatype_new 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 fm = T| F| Le tm | Lt tm | Eq tm | NEq tm|
+datatype_new fm = T| F| Le tm | Lt tm | Eq tm | NEq tm|
NOT fm| And fm fm| Or fm fm| Imp fm fm| Iff fm fm| E fm| A fm
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Sep 09 20:51:36 2014 +0200
@@ -10,7 +10,7 @@
subsection{* Datatype of polynomial expressions *}
-datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly
+datatype_new poly = C Num | Bound nat | Add poly poly | Sub poly poly
| Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
--- a/src/HOL/HOLCF/Discrete.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/HOLCF/Discrete.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports Cont
begin
-datatype 'a discr = Discr "'a :: type"
+datatype_new 'a discr = Discr "'a :: type"
subsection {* Discrete cpo class instance *}
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports IOA Action Lemmas
begin
-datatype 'a abs_action = S 'a | R 'a
+datatype_new 'a abs_action = S 'a | R 'a
(**********************************************************
--- a/src/HOL/HOLCF/IOA/ABP/Action.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/HOLCF/IOA/ABP/Action.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports Packet
begin
-datatype 'm action =
+datatype_new 'm action =
Next | S_msg 'm | R_msg 'm
| S_pkt "'m packet" | R_pkt "'m packet"
| S_ack bool | R_ack bool
--- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports IOA Action
begin
-datatype 'a abs_action = S 'a | R 'a
+datatype_new 'a abs_action = S 'a | R 'a
definition
ch_asig :: "'a abs_action signature" where
--- a/src/HOL/HOLCF/IOA/NTP/Action.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Action.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports Packet
begin
-datatype 'm action = S_msg 'm | R_msg 'm
+datatype_new 'm action = S_msg 'm | R_msg 'm
| S_pkt "'m packet" | R_pkt "'m packet"
| S_ack bool | R_ack bool
| C_m_s | C_m_r | C_r_s | C_r_r 'm
--- a/src/HOL/HOLCF/IOA/Storage/Action.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/HOLCF/IOA/Storage/Action.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports Main
begin
-datatype action = New | Loc nat | Free nat
+datatype_new action = New | Loc nat | Free nat
lemma [cong]: "!!x. x = y ==> case_action a b c x = case_action a b c y"
by simp
--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports Abstraction
begin
-datatype action = INC
+datatype_new action = INC
definition
C_asig :: "action signature" where
--- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports IOA Abstraction
begin
-datatype action = INC
+datatype_new action = INC
definition
C_asig :: "action signature" where
--- a/src/HOL/HOLCF/Up.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/HOLCF/Up.thy Tue Sep 09 20:51:36 2014 +0200
@@ -13,7 +13,7 @@
subsection {* Definition of new type for lifting *}
-datatype 'a u = Ibottom | Iup 'a
+datatype_new 'a u = Ibottom | Iup 'a
type_notation (xsymbols)
u ("(_\<^sub>\<bottom>)" [1000] 999)
--- a/src/HOL/Hoare/Heap.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Hoare/Heap.thy Tue Sep 09 20:51:36 2014 +0200
@@ -10,7 +10,7 @@
subsection "References"
-datatype 'a ref = Null | Ref 'a
+datatype_new 'a ref = Null | Ref 'a
lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
by (induct x) auto
--- a/src/HOL/Hoare_Parallel/Graph.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Hoare_Parallel/Graph.thy Tue Sep 09 20:51:36 2014 +0200
@@ -4,7 +4,7 @@
theory Graph imports Main begin
-datatype node = Black | White
+datatype_new node = Black | White
type_synonym nodes = "node list"
type_synonym edge = "nat \<times> nat"
--- a/src/HOL/Hoare_Parallel/OG_Com.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Com.thy Tue Sep 09 20:51:36 2014 +0200
@@ -14,7 +14,7 @@
datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a
com"} for non-annotated commands. *}
-datatype 'a ann_com =
+datatype_new 'a ann_com =
AnnBasic "('a assn)" "('a \<Rightarrow> 'a)"
| AnnSeq "('a ann_com)" "('a ann_com)"
| AnnCond1 "('a assn)" "('a bexp)" "('a ann_com)" "('a ann_com)"
--- a/src/HOL/Hoare_Parallel/RG_Com.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Com.thy Tue Sep 09 20:51:36 2014 +0200
@@ -12,7 +12,7 @@
type_synonym 'a bexp = "'a set"
-datatype 'a com =
+datatype_new 'a com =
Basic "'a \<Rightarrow>'a"
| Seq "'a com" "'a com"
| Cond "'a bexp" "'a com" "'a com"
--- a/src/HOL/IMP/ACom.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/ACom.thy Tue Sep 09 20:51:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Annotated Commands"
-datatype 'a acom =
+datatype_new 'a acom =
SKIP 'a ("SKIP {_}" 61) |
Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
Seq "('a acom)" "('a acom)" ("_;;//_" [60, 61] 60) |
--- a/src/HOL/IMP/AExp.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/AExp.thy Tue Sep 09 20:51:36 2014 +0200
@@ -9,7 +9,7 @@
type_synonym state = "vname \<Rightarrow> val"
text_raw{*\snip{AExpaexpdef}{2}{1}{% *}
-datatype aexp = N int | V vname | Plus aexp aexp
+datatype_new aexp = N int | V vname | Plus aexp aexp
text_raw{*}%endsnip*}
text_raw{*\snip{AExpavaldef}{1}{2}{% *}
--- a/src/HOL/IMP/ASM.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/ASM.thy Tue Sep 09 20:51:36 2014 +0200
@@ -5,7 +5,7 @@
subsection "Stack Machine"
text_raw{*\snip{ASMinstrdef}{0}{1}{% *}
-datatype instr = LOADI val | LOAD vname | ADD
+datatype_new instr = LOADI val | LOAD vname | ADD
text_raw{*}%endsnip*}
text_raw{*\snip{ASMstackdef}{1}{2}{% *}
--- a/src/HOL/IMP/Abs_Int1_const.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy Tue Sep 09 20:51:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Constant Propagation"
-datatype const = Const val | Any
+datatype_new const = Const val | Any
fun \<gamma>_const where
"\<gamma>_const (Const i) = {i}" |
--- a/src/HOL/IMP/Abs_Int1_parity.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Tue Sep 09 20:51:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Parity Analysis"
-datatype parity = Even | Odd | Either
+datatype_new parity = Even | Odd | Either
text{* Instantiation of class @{class order} with type @{typ parity}: *}
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Tue Sep 09 20:51:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Constant Propagation"
-datatype cval = Const val | Any
+datatype_new cval = Const val | Any
fun rep_cval where
"rep_cval (Const n) = {n}" |
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Tue Sep 09 20:51:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Interval Analysis"
-datatype ivl = I "int option" "int option"
+datatype_new ivl = I "int option" "int option"
text{* We assume an important invariant: arithmetic operations are never
applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j <
--- a/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy Tue Sep 09 20:51:36 2014 +0200
@@ -10,7 +10,7 @@
text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
-datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
+datatype_new 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
fun "fun" where "fun (FunDom f _) = f"
fun dom where "dom (FunDom _ A) = A"
--- a/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/ACom_ITP.thy Tue Sep 09 20:51:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Annotated Commands"
-datatype 'a acom =
+datatype_new 'a acom =
SKIP 'a ("SKIP {_}" 61) |
Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
Seq "('a acom)" "('a acom)" ("_;;//_" [60, 61] 60) |
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Tue Sep 09 20:51:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Constant Propagation"
-datatype const = Const val | Any
+datatype_new const = Const val | Any
fun \<gamma>_const where
"\<gamma>_const (Const n) = {n}" |
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Tue Sep 09 20:51:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Parity Analysis"
-datatype parity = Even | Odd | Either
+datatype_new parity = Even | Odd | Either
text{* Instantiation of class @{class preord} with type @{typ parity}: *}
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Tue Sep 09 20:51:36 2014 +0200
@@ -6,7 +6,7 @@
subsection "Interval Analysis"
-datatype ivl = I "int option" "int option"
+datatype_new ivl = I "int option" "int option"
definition "\<gamma>_ivl i = (case i of
I (Some l) (Some h) \<Rightarrow> {l..h} |
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_State_ITP.thy Tue Sep 09 20:51:36 2014 +0200
@@ -10,7 +10,7 @@
text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
-datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
+datatype_new 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
fun "fun" where "fun (FunDom f xs) = f"
fun dom where "dom (FunDom f xs) = xs"
--- a/src/HOL/IMP/BExp.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/BExp.thy Tue Sep 09 20:51:36 2014 +0200
@@ -2,7 +2,7 @@
subsection "Boolean Expressions"
-datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
+datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
text_raw{*\snip{BExpbvaldef}{1}{2}{% *}
fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
--- a/src/HOL/IMP/C_like.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/C_like.thy Tue Sep 09 20:51:36 2014 +0200
@@ -4,14 +4,14 @@
type_synonym state = "nat \<Rightarrow> nat"
-datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp
+datatype_new aexp = N nat | Deref aexp ("!") | Plus aexp aexp
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> nat" where
"aval (N n) s = n" |
"aval (!a) s = s(aval a s)" |
"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"
-datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
+datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
"bval (Bc v) _ = v" |
@@ -20,7 +20,7 @@
"bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"
-datatype
+datatype_new
com = SKIP
| Assign aexp aexp ("_ ::= _" [61, 61] 61)
| New aexp aexp
--- a/src/HOL/IMP/Compiler.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/Compiler.thy Tue Sep 09 20:51:36 2014 +0200
@@ -43,7 +43,7 @@
subsection "Instructions and Stack Machine"
text_raw{*\snip{instrdef}{0}{1}{% *}
-datatype instr =
+datatype_new instr =
LOADI int | LOAD vname | ADD | STORE vname |
JMP int | JMPLESS int | JMPGE int
text_raw{*}%endsnip*}
--- a/src/HOL/IMP/OO.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/OO.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,13 +8,13 @@
where "f(x,y := z) == f(x := (f x)(y := z))"
type_synonym addr = nat
-datatype ref = null | Ref addr
+datatype_new ref = null | Ref addr
type_synonym obj = "string \<Rightarrow> ref"
type_synonym venv = "string \<Rightarrow> ref"
type_synonym store = "addr \<Rightarrow> obj"
-datatype exp =
+datatype_new exp =
Null |
New |
V string |
--- a/src/HOL/IMP/Poly_Types.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/Poly_Types.thy Tue Sep 09 20:51:36 2014 +0200
@@ -2,7 +2,7 @@
subsection "Type Variables"
-datatype ty = Ity | Rty | TV nat
+datatype_new ty = Ity | Rty | TV nat
text{* Everything else remains the same. *}
--- a/src/HOL/IMP/Types.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/Types.thy Tue Sep 09 20:51:36 2014 +0200
@@ -7,13 +7,13 @@
subsection "Arithmetic Expressions"
-datatype val = Iv int | Rv real
+datatype_new val = Iv int | Rv real
type_synonym vname = string
type_synonym state = "vname \<Rightarrow> val"
text_raw{*\snip{aexptDef}{0}{2}{% *}
-datatype aexp = Ic int | Rc real | V vname | Plus aexp aexp
+datatype_new aexp = Ic int | Rc real | V vname | Plus aexp aexp
text_raw{*}%endsnip*}
inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
@@ -32,7 +32,7 @@
subsection "Boolean Expressions"
-datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
+datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
"tbval (Bc v) s v" |
@@ -44,7 +44,7 @@
subsection "Syntax of Commands"
(* a copy of Com.thy - keep in sync! *)
-datatype
+datatype_new
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
| Seq com com ("_;; _" [60, 61] 60)
@@ -71,7 +71,7 @@
subsection "The Type System"
-datatype ty = Ity | Rty
+datatype_new ty = Ity | Rty
type_synonym tyenv = "vname \<Rightarrow> ty"
--- a/src/HOL/IMP/VCG.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/VCG.thy Tue Sep 09 20:51:36 2014 +0200
@@ -7,7 +7,7 @@
text{* Annotated commands: commands where loops are annotated with
invariants. *}
-datatype acom =
+datatype_new acom =
Askip ("SKIP") |
Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) |
Aseq acom acom ("_;;/ _" [60, 61] 60) |
--- a/src/HOL/IMPP/Com.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMPP/Com.thy Tue Sep 09 20:51:36 2014 +0200
@@ -18,10 +18,10 @@
Arg :: loc and
Res :: loc
-datatype vname = Glb glb | Loc loc
+datatype_new vname = Glb glb | Loc loc
type_synonym globs = "glb => val"
type_synonym locals = "loc => val"
-datatype state = st globs locals
+datatype_new 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 com
+datatype_new com
= SKIP
| Ass vname aexp ("_:==_" [65, 65 ] 60)
| Local loc aexp com ("LOCAL _:=_ IN _" [65, 0, 61] 60)
--- a/src/HOL/IMPP/Hoare.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMPP/Hoare.thy Tue Sep 09 20:51: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 'a triple =
+datatype_new 'a triple =
triple "'a assn" com "'a assn" ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58)
definition
--- a/src/HOL/Imperative_HOL/Heap.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy Tue Sep 09 20:51:36 2014 +0200
@@ -53,8 +53,8 @@
definition empty :: heap where
"empty = \<lparr>arrays = (\<lambda>_ _. []), refs = (\<lambda>_ _. 0), lim = 0\<rparr>"
-datatype 'a array = Array addr
-datatype 'a ref = Ref addr -- "note the phantom type 'a "
+datatype_new 'a array = Array addr
+datatype_new 'a ref = Ref addr -- "note the phantom type 'a "
primrec addr_of_array :: "'a array \<Rightarrow> addr" where
"addr_of_array (Array x) = x"
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Sep 09 20:51:36 2014 +0200
@@ -16,7 +16,7 @@
text {* Monadic heap actions either produce values
and transform the heap, or fail *}
-datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
+datatype_new 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
lemma [code, code del]:
"(Code_Evaluation.term_of :: 'a::typerep Heap \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of"
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Sep 09 20:51:36 2014 +0200
@@ -11,7 +11,7 @@
section {* Definition of Linked Lists *}
setup {* Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a\<Colon>type ref"}) *}
-datatype 'a node = Empty | Node 'a "('a node) ref"
+datatype_new 'a node = Empty | Node 'a "('a node) ref"
primrec
node_encode :: "'a\<Colon>countable node \<Rightarrow> nat"
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Sep 09 20:51:36 2014 +0200
@@ -20,7 +20,7 @@
text {* This resembles exactly to Isat's Proof Steps *}
type_synonym Resolvants = "ClauseId * (Lit * ClauseId) list"
-datatype ProofStep =
+datatype_new ProofStep =
ProofDone bool
| Root ClauseId Clause
| Conflict ClauseId Resolvants
--- a/src/HOL/Induct/ABexp.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Induct/ABexp.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports Main
begin
-datatype 'a aexp =
+datatype_new 'a aexp =
IF "'a bexp" "'a aexp" "'a aexp"
| Sum "'a aexp" "'a aexp"
| Diff "'a aexp" "'a aexp"
--- a/src/HOL/Induct/Comb.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Induct/Comb.thy Tue Sep 09 20:51:36 2014 +0200
@@ -20,7 +20,7 @@
text {* Datatype definition of combinators @{text S} and @{text K}. *}
-datatype comb = K
+datatype_new comb = K
| S
| Ap comb comb (infixl "##" 90)
--- a/src/HOL/Induct/Common_Patterns.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Induct/Common_Patterns.thy Tue Sep 09 20:51:36 2014 +0200
@@ -218,7 +218,7 @@
before!
*}
-datatype foo = Foo1 nat | Foo2 bar
+datatype_new foo = Foo1 nat | Foo2 bar
and bar = Bar1 bool | Bar2 bazar
and bazar = Bazar foo
--- a/src/HOL/Induct/Ordinals.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Induct/Ordinals.thy Tue Sep 09 20:51:36 2014 +0200
@@ -14,7 +14,7 @@
@{url "http://www.dcs.ed.ac.uk/home/pgh/chat.html"}).
*}
-datatype ordinal =
+datatype_new ordinal =
Zero
| Succ ordinal
| Limit "nat => ordinal"
--- a/src/HOL/Induct/PropLog.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Induct/PropLog.thy Tue Sep 09 20:51:36 2014 +0200
@@ -20,7 +20,7 @@
subsection {* The datatype of propositions *}
-datatype 'a pl =
+datatype_new 'a pl =
false |
var 'a ("#_" [1000]) |
imp "'a pl" "'a pl" (infixr "->" 90)
--- a/src/HOL/Induct/Term.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Induct/Term.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports Main
begin
-datatype ('a, 'b) "term" =
+datatype_new ('a, 'b) "term" =
Var 'a
| App 'b "('a, 'b) term list"
--- a/src/HOL/Induct/Tree.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Induct/Tree.thy Tue Sep 09 20:51:36 2014 +0200
@@ -9,7 +9,7 @@
imports Main
begin
-datatype 'a tree =
+datatype_new 'a tree =
Atom 'a
| Branch "nat => 'a tree"
@@ -34,7 +34,7 @@
subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
-datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
+datatype_new brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
text{*Addition of ordinals*}
primrec add :: "[brouwer,brouwer] => brouwer"
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Tue Sep 09 20:51:36 2014 +0200
@@ -31,7 +31,7 @@
consisting of variables, constants, and binary operations on
expressions. *}
-datatype ('adr, 'val) expr =
+datatype_new ('adr, '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 ('adr, 'val) instr =
+datatype_new ('adr, 'val) instr =
Const 'val
| Load 'adr
| Apply "'val binop"
--- a/src/HOL/Isar_Examples/Hoare.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy Tue Sep 09 20:51:36 2014 +0200
@@ -21,7 +21,7 @@
type_synonym 'a bexp = "'a set"
type_synonym 'a assn = "'a set"
-datatype 'a com =
+datatype_new 'a com =
Basic "'a \<Rightarrow> 'a"
| Seq "'a com" "'a com" ("(_;/ _)" [60, 61] 60)
| Cond "'a bexp" "'a com" "'a com"
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Sep 09 20:51:36 2014 +0200
@@ -6,7 +6,7 @@
subsection {* Terms and substitution *}
-datatype ('a, 'b) "term" =
+datatype_new ('a, 'b) "term" =
Var 'a
| App 'b "('a, 'b) term list"
--- a/src/HOL/Lattice/Orders.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Lattice/Orders.thy Tue Sep 09 20:51:36 2014 +0200
@@ -46,7 +46,7 @@
of the original one.
*}
-datatype 'a dual = dual 'a
+datatype_new 'a dual = dual 'a
primrec undual :: "'a dual \<Rightarrow> 'a" where
undual_dual: "undual (dual x) = x"
--- a/src/HOL/Library/Extended.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Library/Extended.thy Tue Sep 09 20:51:36 2014 +0200
@@ -10,7 +10,7 @@
"~~/src/HOL/Library/Simps_Case_Conv"
begin
-datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
+datatype_new 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
instantiation extended :: (order)order
--- a/src/HOL/Library/Extended_Real.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy Tue Sep 09 20:51:36 2014 +0200
@@ -20,7 +20,7 @@
subsection {* Definition and basic properties *}
-datatype ereal = ereal real | PInfty | MInfty
+datatype_new ereal = ereal real | PInfty | MInfty
instantiation ereal :: uminus
begin
--- a/src/HOL/Library/IArray.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Library/IArray.thy Tue Sep 09 20:51: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 'a iarray = IArray "'a list"
+datatype_new 'a iarray = IArray "'a list"
primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
"list_of (IArray xs) = xs"
--- a/src/HOL/Library/Lattice_Constructions.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Library/Lattice_Constructions.thy Tue Sep 09 20:51:36 2014 +0200
@@ -9,7 +9,7 @@
subsection {* Values extended by a bottom element *}
-datatype 'a bot = Value 'a | Bot
+datatype_new 'a bot = Value 'a | Bot
instantiation bot :: (preorder) preorder
begin
@@ -108,7 +108,7 @@
section {* Values extended by a top element *}
-datatype 'a top = Value 'a | Top
+datatype_new '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 'a flat_complete_lattice = Value 'a | Bot | Top
+datatype_new 'a flat_complete_lattice = Value 'a | Bot | Top
instantiation flat_complete_lattice :: (type) order
begin
--- a/src/HOL/Library/Parallel.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Library/Parallel.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
subsection {* Futures *}
-datatype 'a future = fork "unit \<Rightarrow> 'a"
+datatype_new 'a future = fork "unit \<Rightarrow> 'a"
primrec join :: "'a future \<Rightarrow> 'a" where
"join (fork f) = f ()"
--- a/src/HOL/Library/Phantom_Type.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Library/Phantom_Type.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports Main
begin
-datatype ('a, 'b) phantom = phantom 'b
+datatype_new ('a, 'b) phantom = phantom 'b
primrec of_phantom :: "('a, 'b) phantom \<Rightarrow> 'b"
where "of_phantom (phantom x) = x"
--- a/src/HOL/Library/RBT_Impl.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Tue Sep 09 20:51:36 2014 +0200
@@ -16,8 +16,8 @@
subsection {* Datatype of RB trees *}
-datatype color = R | B
-datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
+datatype_new color = R | B
+datatype_new ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
lemma rbt_cases:
obtains (Empty) "t = Empty"
@@ -1728,7 +1728,7 @@
where
"skip_black t = (let t' = skip_red t in case t' of Branch color.B l k v r \<Rightarrow> l | _ \<Rightarrow> t')"
-datatype compare = LT | GT | EQ
+datatype_new compare = LT | GT | EQ
partial_function (tailrec) compare_height :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> compare"
where
--- a/src/HOL/Metis_Examples/Binary_Tree.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Metis_Examples/Binary_Tree.thy Tue Sep 09 20:51:36 2014 +0200
@@ -13,7 +13,7 @@
declare [[metis_new_skolem]]
-datatype 'a bt =
+datatype_new 'a bt =
Lf
| Br 'a "'a bt" "'a bt"
--- a/src/HOL/Metis_Examples/Message.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Metis_Examples/Message.thy Tue Sep 09 20:51:36 2014 +0200
@@ -34,10 +34,10 @@
definition symKeys :: "key set" where
"symKeys == {K. invKey K = K}"
-datatype --{*We allow any number of friendly agents*}
+datatype_new --{*We allow any number of friendly agents*}
agent = Server | Friend nat | Spy
-datatype
+datatype_new
msg = Agent agent --{*Agent names*}
| Number nat --{*Ordinary integers, timestamps, ...*}
| Nonce nat --{*Unguessable nonces*}
--- a/src/HOL/Metis_Examples/Trans_Closure.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy Tue Sep 09 20:51:36 2014 +0200
@@ -15,7 +15,7 @@
type_synonym addr = nat
-datatype val
+datatype_new val
= Unit -- "dummy result value of void expressions"
| Null -- "null reference"
| Bool bool -- "Boolean value"
--- a/src/HOL/MicroJava/DFA/Err.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/MicroJava/DFA/Err.thy Tue Sep 09 20:51:36 2014 +0200
@@ -9,7 +9,7 @@
imports Semilat
begin
-datatype 'a err = Err | OK 'a
+datatype_new 'a err = Err | OK 'a
type_synonym 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
type_synonym 'a esl = "'a set * 'a ord * 'a ebinop"
--- a/src/HOL/MicroJava/J/Example.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Tue Sep 09 20:51:36 2014 +0200
@@ -36,8 +36,8 @@
\end{verbatim}
*}
-datatype cnam' = Base' | Ext'
-datatype vnam' = vee' | x' | e'
+datatype_new cnam' = Base' | Ext'
+datatype_new vnam' = vee' | x' | e'
text {*
@{text cnam'} and @{text vnam'} are intended to be isomorphic
--- a/src/HOL/MicroJava/J/Term.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/MicroJava/J/Term.thy Tue Sep 09 20:51:36 2014 +0200
@@ -6,9 +6,9 @@
theory Term imports Value begin
-datatype binop = Eq | Add -- "function codes for binary operation"
+datatype_new binop = Eq | Add -- "function codes for binary operation"
-datatype expr
+datatype_new expr
= NewC cname -- "class instance creation"
| Cast cname expr -- "type cast"
| Lit val -- "literal value, also references"
@@ -21,7 +21,7 @@
| Call cname expr mname
"ty list" "expr list" ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call"
-datatype stmt
+datatype_new stmt
= Skip -- "empty statement"
| Expr expr -- "expression statement"
| Comp stmt stmt ("_;; _" [61,60]60)
--- a/src/HOL/MicroJava/J/Type.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/MicroJava/J/Type.thy Tue Sep 09 20:51:36 2014 +0200
@@ -45,14 +45,14 @@
end
-- "exceptions"
-datatype
+datatype_new
xcpt
= NullPointer
| ClassCast
| OutOfMemory
-- "class names"
-datatype cname
+datatype_new cname
= Object
| Xcpt xcpt
| Cname cnam
@@ -128,23 +128,23 @@
end
-- "names for @{text This} pointer and local/field variables"
-datatype vname
+datatype_new vname
= This
| VName vnam
-- "primitive type, cf. 4.2"
-datatype prim_ty
+datatype_new prim_ty
= Void -- "'result type' of void methods"
| Boolean
| Integer
-- "reference type, cf. 4.3"
-datatype ref_ty
+datatype_new ref_ty
= NullT -- "null type, cf. 4.1"
| ClassT cname -- "class type"
-- "any type, cf. 4.1"
-datatype ty
+datatype_new ty
= PrimT prim_ty -- "primitive type"
| RefT ref_ty -- "reference type"
--- a/src/HOL/MicroJava/J/Value.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/MicroJava/J/Value.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,11 +8,11 @@
typedecl loc' -- "locations, i.e. abstract references on objects"
-datatype loc
+datatype_new loc
= XcptRef xcpt -- "special locations for pre-allocated system exceptions"
| Loc loc' -- "usual locations (references on objects)"
-datatype val
+datatype_new val
= Unit -- "dummy result value of void methods"
| Null -- "null reference"
| Bool bool -- "Boolean value"
--- a/src/HOL/MicroJava/JVM/JVMDefensive.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/MicroJava/JVM/JVMDefensive.thy Tue Sep 09 20:51:36 2014 +0200
@@ -11,7 +11,7 @@
text {*
Extend the state space by one element indicating a type error (or
other abnormal termination) *}
-datatype 'a type_error = TypeError | Normal 'a
+datatype_new 'a type_error = TypeError | Normal 'a
abbreviation
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
theory JVMInstructions imports JVMState begin
-datatype
+datatype_new
instr = Load nat -- "load from local variable"
| Store nat -- "store into local variable"
| LitPush val -- "push a literal (constant)"
--- a/src/HOL/NanoJava/Decl.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/NanoJava/Decl.thy Tue Sep 09 20:51:36 2014 +0200
@@ -7,7 +7,7 @@
theory Decl imports Term begin
-datatype ty
+datatype_new ty
= NT --{* null type *}
| Class cname --{* class type *}
--- a/src/HOL/NanoJava/State.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/NanoJava/State.thy Tue Sep 09 20:51:36 2014 +0200
@@ -13,7 +13,7 @@
text {* Locations, i.e.\ abstract references to objects *}
typedecl loc
-datatype val
+datatype_new val
= Null --{* null reference *}
| Addr loc --{* address, i.e. location of object *}
--- a/src/HOL/NanoJava/Term.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/NanoJava/Term.thy Tue Sep 09 20:51:36 2014 +0200
@@ -23,7 +23,7 @@
Res_neq_This [simp]: "Res \<noteq> This"
*)
-datatype stmt
+datatype_new stmt
= Skip --{* empty statement *}
| Comp stmt stmt ("_;; _" [91,90 ] 90)
| Cond expr stmt stmt ("If '(_') _ Else _" [ 3,91,91] 91)
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Tue Sep 09 20:51:36 2014 +0200
@@ -44,7 +44,7 @@
nitpick [card = 17, expect = none]
oops
-datatype ('a, 'b) pd = Pd "'a \<times> 'b"
+datatype_new ('a, 'b) pd = Pd "'a \<times> 'b"
fun fs where
"fs (Pd (a, _)) = a"
@@ -76,7 +76,7 @@
nitpick [expect = genuine]
oops
-datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
+datatype_new ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
fun app where
"app (Fn f) x = f x"
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Tue Sep 09 20:51:36 2014 +0200
@@ -206,7 +206,7 @@
nitpick [binary_ints, expect = none]
sorry
-datatype tree = Null | Node nat tree tree
+datatype_new tree = Null | Node nat tree tree
primrec labels where
"labels Null = {}" |
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Sep 09 20:51:36 2014 +0200
@@ -223,7 +223,7 @@
subsection {* 2.10. Boxing *}
-datatype tm = Var nat | Lam tm | App tm tm
+datatype_new 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 alphabet = a | b
+datatype_new alphabet = a | b
inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
"[] \<in> S\<^sub>1"
@@ -381,7 +381,7 @@
subsection {* 3.2. AA Trees *}
-datatype 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
+datatype_new 'a aa_tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a aa_tree" "'a aa_tree"
primrec data where
"data \<Lambda> = undefined" |
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Tue Sep 09 20:51:36 2014 +0200
@@ -617,7 +617,7 @@
text {* Non-recursive datatypes *}
-datatype T1 = A | B
+datatype_new T1 = A | B
lemma "P (x\<Colon>T1)"
nitpick [expect = genuine]
@@ -653,7 +653,7 @@
nitpick [expect = genuine]
oops
-datatype 'a T2 = C T1 | D 'a
+datatype_new 'a T2 = C T1 | D 'a
lemma "P (x\<Colon>'a T2)"
nitpick [expect = genuine]
@@ -685,7 +685,7 @@
nitpick [expect = genuine]
oops
-datatype ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
+datatype_new ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
lemma "P (x\<Colon>('a, 'b) T3)"
nitpick [expect = genuine]
@@ -790,7 +790,7 @@
nitpick [expect = genuine]
oops
-datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
+datatype_new BitList = BitListNil | Bit0 BitList | Bit1 BitList
lemma "P (x\<Colon>BitList)"
nitpick [expect = genuine]
@@ -823,7 +823,7 @@
nitpick [expect = genuine]
oops
-datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
+datatype_new 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
lemma "P (x\<Colon>'a BinTree)"
nitpick [expect = genuine]
@@ -857,7 +857,7 @@
text {* Mutually recursive datatypes *}
-datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
+datatype_new 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
and 'a bexp = Equal "'a aexp" "'a aexp"
lemma "P (x\<Colon>'a aexp)"
@@ -880,17 +880,17 @@
nitpick [expect = genuine]
oops
-lemma "rec_aexp_bexp_1 number ite equal (Number x) = number x"
+lemma "rec_aexp number ite equal (Number x) = number x"
nitpick [card = 1-3, expect = none]
apply simp
done
-lemma "rec_aexp_bexp_1 number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp_bexp_1 number ite equal y) (rec_aexp_bexp_1 number ite equal z)"
+lemma "rec_aexp number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp number ite equal y) (rec_aexp number ite equal z)"
nitpick [card = 1-3, expect = none]
apply simp
done
-lemma "P (rec_aexp_bexp_1 number ite equal x)"
+lemma "P (rec_aexp number ite equal x)"
nitpick [expect = genuine]
oops
@@ -898,7 +898,7 @@
nitpick [expect = genuine]
oops
-lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp_bexp_1 number ite equal x) (rec_aexp_bexp_1 number ite equal y)"
+lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)"
nitpick [card = 1-3, expect = none]
apply simp
done
@@ -911,8 +911,7 @@
nitpick [expect = genuine]
oops
-datatype X = A | B X | C Y
- and Y = D X | E Y | F
+datatype_new X = A | B X | C Y and Y = D X | E Y | F
lemma "P (x\<Colon>X)"
nitpick [expect = genuine]
@@ -958,22 +957,22 @@
nitpick [expect = genuine]
oops
-lemma "rec_X_Y_1 a b c d e f A = a"
+lemma "rec_X a b c d e f A = a"
nitpick [card = 1-5, expect = none]
apply simp
done
-lemma "rec_X_Y_1 a b c d e f (B x) = b x (rec_X_Y_1 a b c d e f x)"
+lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)"
nitpick [card = 1-5, expect = none]
apply simp
done
-lemma "rec_X_Y_1 a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)"
+lemma "rec_X a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)"
nitpick [card = 1-5, expect = none]
apply simp
done
-lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X_Y_1 a b c d e f x)"
+lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X a b c d e f x)"
nitpick [card = 1-5, expect = none]
apply simp
done
@@ -988,7 +987,7 @@
apply simp
done
-lemma "P (rec_X_Y_1 a b c d e f x)"
+lemma "P (rec_X a b c d e f x)"
nitpick [expect = genuine]
oops
@@ -1000,7 +999,7 @@
text {* Indirect recursion is implemented via mutual recursion. *}
-datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
+datatype_new XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
lemma "P (x\<Colon>XOpt)"
nitpick [expect = genuine]
@@ -1014,12 +1013,12 @@
nitpick [expect = genuine]
oops
-lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
+lemma "rec_X cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
nitpick [card = 1-5, expect = none]
apply simp
done
-lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))"
+lemma "rec_X cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))"
nitpick [card = 1-3, expect = none]
apply simp
done
@@ -1029,7 +1028,7 @@
apply simp
done
-lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
+lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_X cx dx n1 s1 n2 s2 x)"
nitpick [card = 1-4, expect = none]
apply simp
done
@@ -1039,12 +1038,12 @@
apply simp
done
-lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
+lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_X cx dx n1 s1 n2 s2 x)"
nitpick [card = 1-4, expect = none]
apply simp
done
-lemma "P (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
+lemma "P (rec_X cx dx n1 s1 n2 s2 x)"
nitpick [expect = genuine]
oops
@@ -1056,7 +1055,7 @@
nitpick [expect = genuine]
oops
-datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
+datatype_new 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
lemma "P (x\<Colon>'a YOpt)"
nitpick [expect = genuine]
@@ -1070,30 +1069,7 @@
nitpick [expect = genuine]
oops
-lemma "rec_YOpt_1 cy n s (CY x) = cy x (rec_YOpt_2 cy n s x)"
-nitpick [card = 1-2, expect = none]
-apply simp
-done
-
-lemma "rec_YOpt_2 cy n s None = n"
-nitpick [card = 1-2, expect = none]
-apply simp
-done
-
-lemma "rec_YOpt_2 cy n s (Some x) = s x (\<lambda>a. rec_YOpt_1 cy n s (x a))"
-nitpick [card = 1-2, expect = none]
-apply simp
-done
-
-lemma "P (rec_YOpt_1 cy n s x)"
-nitpick [expect = genuine]
-oops
-
-lemma "P (rec_YOpt_2 cy n s x)"
-nitpick [expect = genuine]
-oops
-
-datatype Trie = TR "Trie list"
+datatype_new Trie = TR "Trie list"
lemma "P (x\<Colon>Trie)"
nitpick [expect = genuine]
@@ -1107,30 +1083,7 @@
nitpick [expect = genuine]
oops
-lemma "rec_Trie_1 tr nil cons (TR x) = tr x (rec_Trie_2 tr nil cons x)"
-nitpick [card = 1-4, expect = none]
-apply simp
-done
-
-lemma "rec_Trie_2 tr nil cons [] = nil"
-nitpick [card = 1-4, expect = none]
-apply simp
-done
-
-lemma "rec_Trie_2 tr nil cons (x#xs) = cons x xs (rec_Trie_1 tr nil cons x) (rec_Trie_2 tr nil cons xs)"
-nitpick [card = 1-4, expect = none]
-apply simp
-done
-
-lemma "P (rec_Trie_1 tr nil cons x)"
-nitpick [card = 1, expect = genuine]
-oops
-
-lemma "P (rec_Trie_2 tr nil cons x)"
-nitpick [card = 1, expect = genuine]
-oops
-
-datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
+datatype_new InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
lemma "P (x\<Colon>InfTree)"
nitpick [expect = genuine]
@@ -1158,7 +1111,7 @@
nitpick [expect = genuine]
oops
-datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
+datatype_new 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
lemma "P (x\<Colon>'a lambda)"
nitpick [expect = genuine]
@@ -1194,8 +1147,8 @@
text {* Taken from "Inductive datatypes in HOL", p. 8: *}
-datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
-datatype 'c U = E "('c, 'c U) T"
+datatype_new ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
+datatype_new 'c U = E "('c, 'c U) T"
lemma "P (x\<Colon>'c U)"
nitpick [expect = genuine]
@@ -1209,43 +1162,6 @@
nitpick [expect = genuine]
oops
-lemma "rec_U_1 e c d nil cons (E x) = e x (rec_U_2 e c d nil cons x)"
-nitpick [card = 1-3, expect = none]
-apply simp
-done
-
-lemma "rec_U_2 e c d nil cons (C x) = c x"
-nitpick [card = 1-3, expect = none]
-apply simp
-done
-
-lemma "rec_U_2 e c d nil cons (D x) = d x (rec_U_3 e c d nil cons x)"
-nitpick [card = 1-3, expect = none]
-apply simp
-done
-
-lemma "rec_U_3 e c d nil cons [] = nil"
-nitpick [card = 1-3, expect = none]
-apply simp
-done
-
-lemma "rec_U_3 e c d nil cons (x#xs) = cons x xs (rec_U_1 e c d nil cons x) (rec_U_3 e c d nil cons xs)"
-nitpick [card = 1-3, expect = none]
-apply simp
-done
-
-lemma "P (rec_U_1 e c d nil cons x)"
-nitpick [expect = genuine]
-oops
-
-lemma "P (rec_U_2 e c d nil cons x)"
-nitpick [card = 1, expect = genuine]
-oops
-
-lemma "P (rec_U_3 e c d nil cons x)"
-nitpick [card = 1, expect = genuine]
-oops
-
subsubsection {* Records *}
record ('a, 'b) point =
--- a/src/HOL/Nominal/Examples/CK_Machine.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy Tue Sep 09 20:51:36 2014 +0200
@@ -81,7 +81,7 @@
section {* Evaluation Contexts *}
-datatype ctx =
+datatype_new ctx =
Hole ("\<box>")
| CAPPL "ctx" "lam"
| CAPPR "lam" "ctx"
--- a/src/HOL/Nominal/Examples/Pattern.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy Tue Sep 09 20:51:36 2014 +0200
@@ -38,7 +38,7 @@
where
"\<lambda>x:T. t \<equiv> Abs T x t"
-datatype pat =
+datatype_new pat =
PVar name ty
| PTuple pat pat ("(1'\<langle>\<langle>_,/ _'\<rangle>\<rangle>)")
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Sep 09 20:51:36 2014 +0200
@@ -107,7 +107,7 @@
hide_const Pow
-datatype expr = Log expr | Mult expr expr | Div expr expr | x | Num int | Plus expr expr
+datatype_new 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 abc = A | B | C
+datatype_new abc = A | B | C
inductive notB :: "abc => bool"
where
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Tue Sep 09 20:51:36 2014 +0200
@@ -24,7 +24,7 @@
(Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
*}
-datatype alphabet = a | b
+datatype_new alphabet = a | b
inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
"[] \<in> S\<^sub>1"
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy Tue Sep 09 20:51:36 2014 +0200
@@ -10,11 +10,11 @@
text {* a contribution by Aditi Barthwal *}
-datatype ('nts,'ts) symbol = NTS 'nts
+datatype_new ('nts,'ts) symbol = NTS 'nts
| TS 'ts
-datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"
+datatype_new ('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 alphabet = a | b
+datatype_new alphabet = a | b
inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
"[] \<in> S\<^sub>1"
@@ -140,7 +140,7 @@
type_synonym var = nat
type_synonym state = "int list"
-datatype com =
+datatype_new com =
Skip |
Ass var "state => int" |
Seq com com |
@@ -164,11 +164,11 @@
subsection {* Lambda *}
-datatype type =
+datatype_new type =
Atom nat
| Fun type type (infixr "\<Rightarrow>" 200)
-datatype dB =
+datatype_new dB =
Var nat
| App dB dB (infixl "\<degree>" 200)
| Abs type dB
@@ -237,12 +237,12 @@
type_synonym vvalue = int
type_synonym var_assign = "vname \<Rightarrow> vvalue" --"variable assignment"
-datatype ir_expr =
+datatype_new ir_expr =
IrConst vvalue
| ObjAddr vname
| Add ir_expr ir_expr
-datatype val =
+datatype_new val =
IntVal vvalue
record configuration =
@@ -267,14 +267,14 @@
type_synonym name = nat --"For simplicity in examples"
type_synonym state' = "name \<Rightarrow> nat"
-datatype aexp = N nat | V name | Plus aexp aexp
+datatype_new aexp = N nat | V name | Plus aexp aexp
fun aval :: "aexp \<Rightarrow> state' \<Rightarrow> nat" where
"aval (N n) _ = n" |
"aval (V x) st = st x" |
"aval (Plus e\<^sub>1 e\<^sub>2) st = aval e\<^sub>1 st + aval e\<^sub>2 st"
-datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
+datatype_new bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
primrec bval :: "bexp \<Rightarrow> state' \<Rightarrow> bool" where
"bval (B b) _ = b" |
@@ -282,7 +282,7 @@
"bval (And b1 b2) st = (bval b1 st \<and> bval b2 st)" |
"bval (Less a\<^sub>1 a\<^sub>2) st = (aval a\<^sub>1 st < aval a\<^sub>2 st)"
-datatype
+datatype_new
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 proc = nil | pre nat proc | or proc proc | par proc proc
+datatype_new proc = nil | pre nat proc | or proc proc | par proc proc
inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
"step (pre n p) n p" |
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Sep 09 20:51:36 2014 +0200
@@ -2,13 +2,13 @@
imports Main
begin
-datatype guest = Guest0 | Guest1
-datatype key = Key0 | Key1 | Key2 | Key3
-datatype room = Room0
+datatype_new guest = Guest0 | Guest1
+datatype_new key = Key0 | Key1 | Key2 | Key3
+datatype_new room = Room0
type_synonym card = "key * key"
-datatype event =
+datatype_new event =
Check_in guest room card | Enter guest room card | Exit guest room
definition initk :: "room \<Rightarrow> key"
--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy Tue Sep 09 20:51:36 2014 +0200
@@ -11,7 +11,7 @@
type_synonym var = unit
type_synonym state = bool
-datatype com =
+datatype_new com =
Skip |
Ass bool |
Seq com com |
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Tue Sep 09 20:51:36 2014 +0200
@@ -11,7 +11,7 @@
type_synonym var = unit
type_synonym state = bool
-datatype com =
+datatype_new com =
Skip |
Ass bool |
Seq com com |
--- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy Tue Sep 09 20:51:36 2014 +0200
@@ -11,7 +11,7 @@
type_synonym var = unit
type_synonym state = int
-datatype com =
+datatype_new com =
Skip |
Ass var "int" |
Seq com com |
--- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy Tue Sep 09 20:51:36 2014 +0200
@@ -11,7 +11,7 @@
type_synonym var = nat
type_synonym state = "int list"
-datatype com =
+datatype_new com =
Skip |
Ass var "int" |
Seq com com |
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Tue Sep 09 20:51:36 2014 +0200
@@ -4,11 +4,11 @@
subsection {* Lambda *}
-datatype type =
+datatype_new type =
Atom nat
| Fun type type (infixr "\<Rightarrow>" 200)
-datatype dB =
+datatype_new dB =
Var nat
| App dB dB (infixl "\<degree>" 200)
| Abs type dB
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Tue Sep 09 20:51:36 2014 +0200
@@ -53,7 +53,7 @@
section {* Context Free Grammar *}
-datatype alphabet = a | b
+datatype_new alphabet = a | b
inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
"[] \<in> S\<^sub>1"
@@ -179,7 +179,7 @@
type_synonym var = nat
type_synonym state = "int list"
-datatype com =
+datatype_new com =
Skip |
Ass var "int" |
Seq com com |
@@ -206,11 +206,11 @@
subsection {* Lambda *}
-datatype type =
+datatype_new type =
Atom nat
| Fun type type (infixr "\<Rightarrow>" 200)
-datatype dB =
+datatype_new dB =
Var nat
| App dB dB (infixl "\<degree>" 200)
| Abs type dB
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Tue Sep 09 20:51:36 2014 +0200
@@ -139,7 +139,7 @@
subsection {* Alternative Rules *}
-datatype char = C | D | E | F | G | H
+datatype_new 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 com =
+datatype_new 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 proc = nil | pre nat proc | or proc proc | par proc proc
+datatype_new proc = nil | pre nat proc | or proc proc | par proc proc
inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
where
@@ -974,7 +974,7 @@
*)
subsection {* AVL Tree *}
-datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
+datatype_new '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 ErrorObject = Error String.literal int
+datatype_new ErrorObject = Error String.literal int
inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
where
@@ -1508,7 +1508,7 @@
text {* The higher-order predicate r is in an output term *}
-datatype result = Result bool
+datatype_new result = Result bool
inductive fixed_relation :: "'a => bool"
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Tue Sep 09 20:51:36 2014 +0200
@@ -9,7 +9,7 @@
manually slightly adapted.
*}
-datatype Nat = Zer
+datatype_new Nat = Zer
| Suc Nat
fun sub :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat"
@@ -20,10 +20,10 @@
Zer \<Rightarrow> Zer
| Suc x' \<Rightarrow> sub x' y')"
-datatype Sym = N0
+datatype_new Sym = N0
| N1 Sym
-datatype RE = Sym Sym
+datatype_new RE = Sym Sym
| Or RE RE
| Seq RE RE
| And RE RE
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Tue Sep 09 20:51:36 2014 +0200
@@ -107,13 +107,13 @@
"unique [] = True"
| "unique (x # xs) = (xs\<langle>fst x\<rangle>\<^sub>? = \<bottom> \<and> unique xs)"
-datatype type =
+datatype_new type =
TVar nat
| Top
| Fun type type (infixr "\<rightarrow>" 200)
| TyAll type type ("(3\<forall><:_./ _)" [0, 10] 10)
-datatype binding = VarB type | TVarB type
+datatype_new binding = VarB type | TVarB type
type_synonym env = "binding list"
primrec is_TVarB :: "binding \<Rightarrow> bool"
@@ -131,7 +131,7 @@
"mapB f (VarB T) = VarB (f T)"
| "mapB f (TVarB T) = TVarB (f T)"
-datatype trm =
+datatype_new trm =
Var nat
| Abs type trm ("(3\<lambda>:_./ _)" [0, 10] 10)
| TAbs type trm ("(3\<lambda><:_./ _)" [0, 10] 10)
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Tue Sep 09 20:51:36 2014 +0200
@@ -2,7 +2,7 @@
imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
begin
-datatype agent = Alice | Bob | Spy
+datatype_new agent = Alice | Bob | Spy
definition agents :: "agent set"
where
@@ -12,14 +12,14 @@
where
"bad = {Spy}"
-datatype key = pubEK agent | priEK agent
+datatype_new key = pubEK agent | priEK agent
fun invKey
where
"invKey (pubEK A) = priEK A"
| "invKey (priEK A) = pubEK A"
-datatype
+datatype_new
msg = Agent agent
| Key key
| Nonce nat
@@ -73,7 +73,7 @@
| initState_Spy:
"initState Spy = (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)"
-datatype
+datatype_new
event = Says agent agent msg
| Gets agent msg
| Notes agent msg
--- a/src/HOL/Statespace/DistinctTreeProver.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Tue Sep 09 20:51:36 2014 +0200
@@ -18,7 +18,7 @@
subsection {* The Binary Tree *}
-datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip
+datatype_new 'a tree = Node "'a tree" 'a bool "'a tree" | Tip
text {* The boolean flag in the node marks the content of the node as
--- a/src/HOL/TLA/Inc/Inc.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy Tue Sep 09 20:51:36 2014 +0200
@@ -9,7 +9,7 @@
begin
(* program counter as an enumeration type *)
-datatype pcount = a | b | g
+datatype_new pcount = a | b | g
axiomatization
(* program variables *)
--- a/src/HOL/TLA/Memory/MemClerkParameters.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/TLA/Memory/MemClerkParameters.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports RPCParameters
begin
-datatype mClkState = clkA | clkB
+datatype_new mClkState = clkA | clkB
(* types sent on the clerk's send and receive channels are argument types
of the memory and the RPC, respectively *)
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports Memory RPC MemClerk
begin
-datatype histState = histA | histB
+datatype_new histState = histA | histB
type_synonym histType = "(PrIds => histState) stfun" (* the type of the history variable *)
--- a/src/HOL/TLA/Memory/MemoryParameters.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy Tue Sep 09 20:51:36 2014 +0200
@@ -9,7 +9,7 @@
begin
(* the memory operations *)
-datatype memOp = read Locs | "write" Locs Vals
+datatype_new memOp = read Locs | "write" Locs Vals
consts
(* memory locations and contents *)
--- a/src/HOL/TLA/Memory/RPCParameters.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/TLA/Memory/RPCParameters.thy Tue Sep 09 20:51:36 2014 +0200
@@ -13,8 +13,8 @@
memory implementation.
*)
-datatype rpcOp = memcall memOp | othercall Vals
-datatype rpcState = rpcA | rpcB
+datatype_new rpcOp = memcall memOp | othercall Vals
+datatype_new rpcState = rpcA | rpcB
consts
(* some particular return values *)
--- a/src/HOL/UNITY/Comp/Counter.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/UNITY/Comp/Counter.thy Tue Sep 09 20:51:36 2014 +0200
@@ -13,7 +13,7 @@
theory Counter imports "../UNITY_Main" begin
(* Variables are names *)
-datatype name = C | c nat
+datatype_new name = C | c nat
type_synonym state = "name=>int"
primrec sum :: "[nat,state]=>int" where
--- a/src/HOL/UNITY/Simple/Network.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/UNITY/Simple/Network.thy Tue Sep 09 20:51:36 2014 +0200
@@ -11,9 +11,9 @@
(*The state assigns a number to each process variable*)
-datatype pvar = Sent | Rcvd | Idle
+datatype_new pvar = Sent | Rcvd | Idle
-datatype pname = Aproc | Bproc
+datatype_new pname = Aproc | Bproc
type_synonym state = "pname * pvar => nat"
--- a/src/HOL/UNITY/Simple/Token.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/UNITY/Simple/Token.thy Tue Sep 09 20:51:36 2014 +0200
@@ -15,7 +15,7 @@
subsection{*Definitions*}
-datatype pstate = Hungry | Eating | Thinking
+datatype_new pstate = Hungry | Eating | Thinking
--{*process states*}
record state =
--- a/src/HOL/Unix/Nested_Environment.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Unix/Nested_Environment.thy Tue Sep 09 20:51:36 2014 +0200
@@ -19,7 +19,7 @@
position within the structure.
*}
-datatype ('a, 'b, 'c) env =
+datatype_new ('a, 'b, 'c) env =
Val 'a
| Env 'b "'c \<Rightarrow> ('a, 'b, 'c) env option"
--- a/src/HOL/Unix/Unix.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Unix/Unix.thy Tue Sep 09 20:51:36 2014 +0200
@@ -73,7 +73,7 @@
\cite{Naraschewski:2001}.}
*}
-datatype perm =
+datatype_new perm =
Readable
| Writable
| Executable -- "(ignored)"
@@ -284,7 +284,7 @@
@{text "root \<midarrow>x\<rightarrow> root'"} for the operational semantics.
*}
-datatype operation =
+datatype_new operation =
Read uid string path
| Write uid string path
| Chmod uid perms path
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy Tue Sep 09 20:51:36 2014 +0200
@@ -19,7 +19,7 @@
subsection {* Plain Ad Hoc Overloading *}
text {*Consider the type of first-order terms.*}
-datatype ('a, 'b) "term" =
+datatype_new ('a, 'b) "term" =
Var 'b |
Fun 'a "('a, 'b) term list"
--- a/src/HOL/ex/BT.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/BT.thy Tue Sep 09 20:51:36 2014 +0200
@@ -9,7 +9,7 @@
theory BT imports Main begin
-datatype 'a bt =
+datatype_new 'a bt =
Lf
| Br 'a "'a bt" "'a bt"
--- a/src/HOL/ex/Chinese.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Chinese.thy Tue Sep 09 20:51:36 2014 +0200
@@ -16,7 +16,7 @@
*}
-datatype shuzi =
+datatype_new shuzi =
One ("一")
| Two ("二")
| Three ("三")
--- a/src/HOL/ex/Eval_Examples.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Eval_Examples.thy Tue Sep 09 20:51:36 2014 +0200
@@ -42,7 +42,7 @@
text {* a fancy datatype *}
-datatype ('a, 'b) foo =
+datatype_new ('a, 'b) foo =
Foo "'a\<Colon>order" 'b
| Bla "('a, 'b) bar"
| Dummy nat
--- a/src/HOL/ex/Fundefs.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Fundefs.thy Tue Sep 09 20:51:36 2014 +0200
@@ -372,7 +372,7 @@
(* Simple Higher-Order Recursion *)
-datatype 'a tree =
+datatype_new 'a tree =
Leaf 'a
| Branch "'a tree list"
@@ -423,7 +423,7 @@
(* Many equations (quadratic blowup) *)
-datatype DT =
+datatype_new DT =
A | B | C | D | E | F | G | H | I | J | K | L | M | N | P
| Q | R | S | T | U | V
--- a/src/HOL/ex/Hebrew.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Hebrew.thy Tue Sep 09 20:51:36 2014 +0200
@@ -12,7 +12,7 @@
text {* The Hebrew Alef-Bet (א-ב). *}
-datatype alef_bet =
+datatype_new alef_bet =
Alef ("א")
| Bet ("ב")
| Gimel ("ג")
--- a/src/HOL/ex/Normalization_by_Evaluation.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy Tue Sep 09 20:51: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 n = Z | S n
+datatype_new n = Z | S n
primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where
"add Z = id"
--- a/src/HOL/ex/Records.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Records.thy Tue Sep 09 20:51:36 2014 +0200
@@ -166,7 +166,7 @@
subsection {* Coloured points: record extension *}
-datatype colour = Red | Green | Blue
+datatype_new colour = Red | Green | Blue
record cpoint = point +
colour :: colour
--- a/src/HOL/ex/Reflection_Examples.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Reflection_Examples.thy Tue Sep 09 20:51:36 2014 +0200
@@ -46,7 +46,7 @@
text {* Example 1 : Propositional formulae and NNF. *}
text {* The type @{text fm} represents simple propositional formulae: *}
-datatype form = TrueF | FalseF | Less nat nat
+datatype_new form = TrueF | FalseF | Less nat nat
| And form form | Or form form | Neg form | ExQ form
primrec interp :: "form \<Rightarrow> ('a::ord) list \<Rightarrow> bool"
@@ -66,7 +66,7 @@
apply reify
oops
-datatype fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
+datatype_new fm = And fm fm | Or fm fm | Imp fm fm | Iff fm fm | NOT fm | At nat
primrec Ifm :: "fm \<Rightarrow> bool list \<Rightarrow> bool"
where
@@ -135,7 +135,7 @@
text {* Example 2: Simple arithmetic formulae *}
text {* The type @{text num} reflects linear expressions over natural number *}
-datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
+datatype_new num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num
text {* This is just technical to make recursive definitions easier. *}
primrec num_size :: "num \<Rightarrow> nat"
@@ -252,7 +252,7 @@
text {* Let's lift this to formulae and see what happens *}
-datatype aform = Lt num num | Eq num num | Ge num num | NEq num num |
+datatype_new aform = Lt num num | Eq num num | Ge num num | NEq num num |
Conj aform aform | Disj aform aform | NEG aform | T | F
primrec linaformsize:: "aform \<Rightarrow> nat"
@@ -331,7 +331,7 @@
one envornement of different types and show that automatic reification also deals with
bindings *}
-datatype rb = BC bool | BAnd rb rb | BOr rb rb
+datatype_new rb = BC bool | BAnd rb rb | BOr rb rb
primrec Irb :: "rb \<Rightarrow> bool"
where
@@ -343,7 +343,7 @@
apply (reify Irb.simps)
oops
-datatype rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
+datatype_new rint = IC int | IVar nat | IAdd rint rint | IMult rint rint
| INeg rint | ISub rint rint
primrec Irint :: "rint \<Rightarrow> int list \<Rightarrow> int"
@@ -370,7 +370,7 @@
apply (reify Irint_simps ("(3::int) * x + y * y - 9 + (- z)"))
oops
-datatype rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
+datatype_new rlist = LVar nat | LEmpty | LCons rint rlist | LAppend rlist rlist
primrec Irlist :: "rlist \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> int list"
where
@@ -387,7 +387,7 @@
apply (reify Irlist.simps Irint_simps ("([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs"))
oops
-datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
+datatype_new rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat
| NNeg rnat | NSub rnat rnat | Nlgth rlist
primrec Irnat :: "rnat \<Rightarrow> int list \<Rightarrow> int list list \<Rightarrow> nat list \<Rightarrow> nat"
@@ -418,7 +418,7 @@
("Suc n * length (([(3::int) * x + y * y - 9 + (- z)] @ []) @ xs)"))
oops
-datatype rifm = RT | RF | RVar nat
+datatype_new 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 prod = Zero | One | Var nat | Mul prod prod
+datatype_new prod = Zero | One | Var nat | Mul prod prod
| Pw prod nat | PNM nat nat prod
primrec Iprod :: " prod \<Rightarrow> ('a::linordered_idom) list \<Rightarrow>'a"
@@ -463,7 +463,7 @@
| "Iprod (Pw a n) vs = Iprod a vs ^ n"
| "Iprod (PNM n k t) vs = (vs ! n) ^ k * Iprod t vs"
-datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F
+datatype_new sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F
| Or sgn sgn | And sgn sgn
primrec Isgn :: "sgn \<Rightarrow> ('a::linordered_idom) list \<Rightarrow> bool"
--- a/src/HOL/ex/Seq.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Seq.thy Tue Sep 09 20:51:36 2014 +0200
@@ -8,7 +8,7 @@
imports Main
begin
-datatype 'a seq = Empty | Seq 'a "'a seq"
+datatype_new 'a seq = Empty | Seq 'a "'a seq"
fun conc :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq"
where
--- a/src/HOL/ex/Serbian.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Serbian.thy Tue Sep 09 20:51:36 2014 +0200
@@ -11,7 +11,7 @@
begin
text{* Serbian cyrillic letters *}
-datatype azbuka =
+datatype_new azbuka =
azbA ("А")
| azbB ("Б")
| azbV ("В")
@@ -47,7 +47,7 @@
thm azbuka.induct
text{* Serbian latin letters *}
-datatype abeceda =
+datatype_new abeceda =
abcA ("A")
| abcB ("B")
| abcC ("C")
--- a/src/HOL/ex/Termination.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Termination.thy Tue Sep 09 20:51:36 2014 +0200
@@ -118,7 +118,7 @@
subsection {* Simple examples with other datatypes than nat, e.g. trees and lists *}
-datatype tree = Node | Branch tree tree
+datatype_new tree = Node | Branch tree tree
fun g_tree :: "tree * tree \<Rightarrow> tree"
where
--- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy Tue Sep 09 20:51:36 2014 +0200
@@ -6,7 +6,7 @@
imports "~~/src/HOL/Library/Transitive_Closure_Table"
begin
-datatype ty = A | B | C
+datatype_new ty = A | B | C
inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
where
--- a/src/HOL/ex/Tree23.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Tree23.thy Tue Sep 09 20:51:36 2014 +0200
@@ -21,16 +21,16 @@
type_synonym key = int -- {*for simplicity, should be a type class*}
-datatype ord = LESS | EQUAL | GREATER
+datatype_new ord = LESS | EQUAL | GREATER
definition "ord i j = (if i<j then LESS else if i=j then EQUAL else GREATER)"
-datatype 'a tree23 =
+datatype_new 'a tree23 =
Empty |
Branch2 "'a tree23" "key * 'a" "'a tree23" |
Branch3 "'a tree23" "key * 'a" "'a tree23" "key * 'a" "'a tree23"
-datatype 'a growth =
+datatype_new 'a growth =
Stay "'a tree23" |
Sprout "'a tree23" "key * 'a" "'a tree23"
@@ -402,7 +402,7 @@
text{* This is a little test harness and should be commented out once the
above functions have been proved correct. *}
-datatype 'a act = Add int 'a | Del int
+datatype_new 'a act = Add int 'a | Del int
fun exec where
"exec [] t = t" |
--- a/src/HOL/ex/Unification.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Unification.thy Tue Sep 09 20:51:36 2014 +0200
@@ -32,7 +32,7 @@
text {* Binary trees with leaves that are constants or variables. *}
-datatype 'a trm =
+datatype_new 'a trm =
Var 'a
| Const 'a
| Comb "'a trm" "'a trm" (infix "\<cdot>" 60)