src/Pure/General/basics.ML
changeset 71116 aa1338a778c1
parent 62505 9e2a65912111
child 78062 edb195122938
equal deleted inserted replaced
71115:3199c08e6413 71116:aa1338a778c1