src/Pure/basis.ML
changeset 3770 294b5905f4eb
parent 3244 71b760618f30
child 5021 235f8508d440
equal deleted inserted replaced
3769:931c336b0707 3770:294b5905f4eb