| changeset 36504 | 7cc639e20cb2 |
| parent 21624 | 6f79647cf536 |
| child 41589 | bbd861837ebc |
--- a/src/HOL/TLA/Memory/MemoryParameters.thy Thu Apr 29 11:05:13 2010 +0200 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy Thu Apr 29 16:53:08 2010 +0200 @@ -12,7 +12,7 @@ begin (* the memory operations *) -datatype memOp = read Locs | write Locs Vals +datatype memOp = read Locs | "write" Locs Vals consts (* memory locations and contents *)