src/HOL/Import/HOL/rich_list.imp
changeset 37146 f652333bbf8e
parent 33640 0d82107dc07a
child 44763 b50d5d694838
equal deleted inserted replaced
37145:01aa36932739 37146:f652333bbf8e