src/HOL/Import/HOL/rich_list.imp
changeset 24546 c90cee3163b7
parent 17188 a26a4fc323ed
child 33640 0d82107dc07a
equal deleted inserted replaced
24545:f406a5744756 24546:c90cee3163b7