indexing description: "[ Shared history. ]" date: "$Date$" revision: "$Revision$" class SHARED_HISTORY feature {NONE} -- Implementation history: HISTORY is -- History of executed commands. once create Result.make ensure history_created: Result /= Void end end