--- a/src/HOL/Datatype_Benchmark/Brackin.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Datatype_Benchmark/Brackin.thy Thu Sep 11 19:18:23 2014 +0200
@@ -1,17 +1,17 @@
(* Title: HOL/Datatype_Benchmark/Brackin.thy
-A couple from Steve Brackin's work.
+A couple of datatypes from Steve Brackin's work.
*)
theory Brackin imports Main begin
-old_datatype T =
+datatype T =
X1 | X2 | X3 | X4 | X5 | X6 | X7 | X8 | X9 | X10 | X11 |
X12 | X13 | X14 | X15 | X16 | X17 | X18 | X19 | X20 | X21 |
X22 | X23 | X24 | X25 | X26 | X27 | X28 | X29 | X30 | X31 |
X32 | X33 | X34
-old_datatype ('a, 'b, 'c) TY1 =
+datatype ('a, 'b, 'c) TY1 =
NoF
| Fk 'a "('a, 'b, 'c) TY2"
and ('a, 'b, 'c) TY2 =
--- a/src/HOL/Datatype_Benchmark/Instructions.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Datatype_Benchmark/Instructions.thy Thu Sep 11 19:18:23 2014 +0200
@@ -5,9 +5,9 @@
theory Instructions imports Main begin
-old_datatype Size = Byte | Word | Long
+datatype Size = Byte | Word | Long
-old_datatype DataRegister =
+datatype DataRegister =
RegD0
| RegD1
| RegD2
@@ -17,7 +17,7 @@
| RegD6
| RegD7
-old_datatype AddressRegister =
+datatype AddressRegister =
RegA0
| RegA1
| RegA2
@@ -27,11 +27,11 @@
| RegA6
| RegA7
-old_datatype DataOrAddressRegister =
+datatype DataOrAddressRegister =
data DataRegister
| address AddressRegister
-old_datatype Condition =
+datatype Condition =
Hi
| Ls
| Cc
@@ -47,7 +47,7 @@
| Gt
| Le
-old_datatype AddressingMode =
+datatype AddressingMode =
immediate nat
| direct DataOrAddressRegister
| indirect AddressRegister
@@ -59,7 +59,7 @@
| pcdisp nat
| pcindex nat DataOrAddressRegister Size
-old_datatype M68kInstruction =
+datatype M68kInstruction =
ABCD AddressingMode AddressingMode
| ADD Size AddressingMode AddressingMode
| ADDA Size AddressingMode AddressRegister