src/Pure/basis.ML
changeset 14706 71590b7733b7
parent 13037 f7f29f8380ce