src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 60565 b7ee41f72add
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Sep 11 19:26:59 2014 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Sep 11 19:32:36 2014 +0200
     1.3 @@ -139,7 +139,7 @@
     1.4  
     1.5  subsection {* Alternative Rules *}
     1.6  
     1.7 -datatype_new char = C | D | E | F | G | H
     1.8 +datatype char = C | D | E | F | G | H
     1.9  
    1.10  inductive is_C_or_D
    1.11  where
    1.12 @@ -784,7 +784,7 @@
    1.13  type_synonym var = nat
    1.14  type_synonym state = "int list"
    1.15  
    1.16 -datatype_new com =
    1.17 +datatype com =
    1.18    Skip |
    1.19    Ass var "state => int" |
    1.20    Seq com com |
    1.21 @@ -809,7 +809,7 @@
    1.22  text{* This example formalizes finite CCS processes without communication or
    1.23  recursion. For simplicity, labels are natural numbers. *}
    1.24  
    1.25 -datatype_new proc = nil | pre nat proc | or proc proc | par proc proc
    1.26 +datatype proc = nil | pre nat proc | or proc proc | par proc proc
    1.27  
    1.28  inductive tupled_step :: "(proc \<times> nat \<times> proc) \<Rightarrow> bool"
    1.29  where
    1.30 @@ -974,7 +974,7 @@
    1.31  *)
    1.32  subsection {* AVL Tree *}
    1.33  
    1.34 -datatype_new 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
    1.35 +datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
    1.36  fun height :: "'a tree => nat" where
    1.37  "height ET = 0"
    1.38  | "height (MKT x l r h) = max (height l) (height r) + 1"
    1.39 @@ -1403,7 +1403,7 @@
    1.40  
    1.41  thm is_error'.equation
    1.42  
    1.43 -datatype_new ErrorObject = Error String.literal int
    1.44 +datatype ErrorObject = Error String.literal int
    1.45  
    1.46  inductive is_error'' :: "ErrorObject \<Rightarrow> bool"
    1.47  where
    1.48 @@ -1508,7 +1508,7 @@
    1.49  
    1.50  text {* The higher-order predicate r is in an output term *}
    1.51  
    1.52 -datatype_new result = Result bool
    1.53 +datatype result = Result bool
    1.54  
    1.55  inductive fixed_relation :: "'a => bool"
    1.56