class interface HTML create make feature make feature -- Add new options add_option (an_option: STRING) require an_option /= void feature -- Routines out attributes_out: STRING -- Was declared in HTML as synonym of body_attributes_out. body_attributes_out: STRING -- Was declared in HTML as synonym of attributes_out. body_out: STRING head_out: STRING out: STRING feature -- Set set_title (s: STRING) feature -- Wipe out wipe_out invariant -- from ANY reflexive_equality: standard_is_equal (Current) reflexive_conformance: conforms_to (Current) end -- class HTML