src/HOL/Import/seq.ML
changeset 38861 27c7b620758c
parent 32960 69916a850301
child 40627 becf5d5187cc
equal deleted inserted replaced
38860:749d09f52fde 38861:27c7b620758c