src/Pure/search.ML
changeset 81473 53e61087bc6f
parent 62919 9eb0359d6a77
child 81954 6f2bcdfa9a19
equal deleted inserted replaced
81472:e43bff789ac0 81473:53e61087bc6f