--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Sep 11 19:32:36 2014 +0200
@@ -139,7 +139,7 @@
subsection {* Alternative Rules *}
-datatype_new char = C | D | E | F | G | H
+datatype char = C | D | E | F | G | H
inductive is_C_or_D
where
@@ -784,7 +784,7 @@
type_synonym var = nat
type_synonym state = "int list"
-datatype_new com =
+datatype com =
Skip |
Ass var "state => int" |
Seq com com |
@@ -809,7 +809,7 @@
text{* This example formalizes finite CCS processes without communication or
recursion. For simplicity, labels are natural numbers. *}
-datatype_new proc = nil | pre nat proc | or proc proc | par proc proc
+datatype proc = nil | pre nat proc | or proc proc | par proc proc
inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
where
@@ -974,7 +974,7 @@
*)
subsection {* AVL Tree *}
-datatype_new 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
+datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
fun height :: "'a tree => nat" where
"height ET = 0"
| "height (MKT x l r h) = max (height l) (height r) + 1"
@@ -1403,7 +1403,7 @@
thm is_error'.equation
-datatype_new ErrorObject = Error String.literal int
+datatype ErrorObject = Error String.literal int
inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
where
@@ -1508,7 +1508,7 @@
text {* The higher-order predicate r is in an output term *}
-datatype_new result = Result bool
+datatype result = Result bool
inductive fixed_relation :: "'a => bool"