indexing description: "Command histories" author: "Patrick Schoenbach" deferred class interface COMMAND_HISTORY feature -- Status report is_executed: BOOLEAN -- Has current item been executed? feature -- Basic operations redo -- Redo command. undo -- Undo command. invariant -- from GENERAL reflexive_equality: standard_is_equal (Current); reflexive_conformance: conforms_to (Current); end -- class COMMAND_HISTORY