# HG changeset patch # User haftmann # Date 1206010873 -3600 # Node ID d5125a62f8397c7587adb863e5294e64b7bf47fe # Parent a170a190c5d33d9b7a6a37e7af5b54be20f430c8 tuned import diff -r a170a190c5d3 -r d5125a62f839 src/HOL/TLA/Memory/ProcedureInterface.thy --- a/src/HOL/TLA/Memory/ProcedureInterface.thy Thu Mar 20 12:01:12 2008 +0100 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Thu Mar 20 12:01:13 2008 +0100 @@ -8,7 +8,7 @@ header {* Procedure interface for RPC-Memory components *} theory ProcedureInterface -imports TLA RPCMemoryParams +imports "../TLA" RPCMemoryParams begin typedecl