--- a/Admin/Benchmarks/HOL-datatype/Instructions.thy Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/Instructions.thy Fri Aug 27 10:54:31 1999 +0200
@@ -2,7 +2,7 @@
ID: $Id$
*)
-Instructions = Main +
+theory Instructions = Main:
(* ------------------------------------------------------------------------- *)
(* Example from Konrad: 68000 instruction set. *)
@@ -117,8 +117,8 @@
| 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