src/Pure/basis.ML
changeset 4314 a6eb21e10090
parent 3244 71b760618f30
child 5021 235f8508d440