src/HOL/List.ML
changeset 12896 4518acda6d93
parent 12887 d25b43743e10
child 13096 04f8cbd1b500
equal deleted inserted replaced
12895:d9dd528ecea6 12896:4518acda6d93