# HG changeset patch # User blanchet # Date 1410455903 -7200 # Node ID 8172bbb37b0622de69102889bc5235f06b21ef7d # Parent 117ba6cbe4140f507d8a09d1f79499f5db78a57e use new datatypes for benchmarks diff -r 117ba6cbe414 -r 8172bbb37b06 src/HOL/Datatype_Benchmark/Brackin.thy --- 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 = diff -r 117ba6cbe414 -r 8172bbb37b06 src/HOL/Datatype_Benchmark/Instructions.thy --- 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