src/Pure/basis.ML
changeset 13510 0a0f37f9c031
parent 13037 f7f29f8380ce
equal deleted inserted replaced
13509:6f168374652a 13510:0a0f37f9c031