src/Pure/basis.ML
changeset 13510 0a0f37f9c031
parent 13037 f7f29f8380ce