src/Pure/basis.ML
changeset 5526 e7617b57a3e6
parent 5208 cea0adbc7276
child 5643 983ce1421211