src/HOL/Import/mono_seq.ML
changeset 32130 2a0645733185
parent 19093 6d584f9d2021
child 32960 69916a850301
equal deleted inserted replaced
32129:d2aea34845d4 32130:2a0645733185