src/Pure/basis.ML
changeset 5417 1f533238b53b
parent 5208 cea0adbc7276
child 5643 983ce1421211