src/Pure/basis.ML
changeset 13457 7ddcf40a80b3
parent 13037 f7f29f8380ce