src/HOL/List.ML
changeset 5807 bd2d9dd34dfd
parent 5758 27a2b36efd95
child 5983 79e301a6a51b