src/Pure/General/ord_list.ML
changeset 38480 e5eed57913d0
parent 33037 b22e44496dc2
child 39687 4e9b6ada3a21