src/Pure/basis.ML
changeset 13713 34ef15959ce7
parent 13037 f7f29f8380ce