src/HOL/Import/mono_seq.ML
changeset 37380 35815ce9218a
parent 32960 69916a850301
child 41589 bbd861837ebc
equal deleted inserted replaced
37379:f23e60581eb3 37380:35815ce9218a