src/Pure/sorts.ML
changeset 21434 944f80576be0
parent 20573 c945a208e7f8
child 21926 1091904ddb19
equal deleted inserted replaced
21433:89104dca628e 21434:944f80576be0