src/HOL/List.ML
changeset 5126 01cbf154d926
parent 5122 229190f9f303
child 5129 99ffd3dfb180