src/Pure/General/basics.ML
changeset 63450 afd657fffdf9
parent 62505 9e2a65912111
child 78062 edb195122938
equal deleted inserted replaced
63449:b3f6e81cd13b 63450:afd657fffdf9