diff -r f6335d319e9f -r db63752140c7 src/HOL/TLA/Memory/RPCMemoryParams.thy --- a/src/HOL/TLA/Memory/RPCMemoryParams.thy Mon Feb 08 13:02:42 1999 +0100 +++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy Mon Feb 08 13:02:56 1999 +0100 @@ -12,9 +12,9 @@ RPCMemoryParams = HOL + types - bit = "bool" (* signal wires for the procedure interface *) - (* Defined as bool for simplicity. All I should really need is *) - (* the existence of two distinct values. *) + bit = "bool" (* Signal wires for the procedure interface. + Defined as bool for simplicity. All I should really need is + the existence of two distinct values. *) Locs (* "syntactic" value type *) Vals (* "syntactic" value type *) PrIds (* process id's *)