src/Pure/basis.ML
changeset 13049 ce180e5b7fa0
parent 13037 f7f29f8380ce