Admin/Benchmarks/HOL-datatype/Instructions.thy

 (*  Title:      Admin/Benchmarks/HOL-datatype/Instructions.thy
     ID:         $Id$
 *)
 
-Instructions = Main +
+theory Instructions = Main:
 
 (* ------------------------------------------------------------------------- *)
 (* Example from Konrad: 68000 instruction set.                               *)
 (* ------------------------------------------------------------------------- *)
 

     | MOVEtoSR AddressingMode
     | MOVEfromSR AddressingMode
     | MOVEtoUSP AddressingMode
     | MOVEfromUSP AddressingMode
     | MOVEA Size AddressingMode AddressRegister
-    | MOVEMto Size AddressingMode (DataOrAddressRegister list)
-    | MOVEMfrom Size (DataOrAddressRegister list) AddressingMode
+    | MOVEMto Size AddressingMode "DataOrAddressRegister list"
+    | MOVEMfrom Size "DataOrAddressRegister list" AddressingMode
     | MOVEP Size AddressingMode AddressingMode
     | MOVEQ nat DataRegister
     | MULS AddressingMode DataRegister
     | MULU AddressingMode DataRegister
     | NBCD AddressingMode