src/Pure/General/scan.ML
changeset 56407 8e7ebc4b30f1
parent 55104 8284c0d5bf52
child 58850 1bb0ad7827b4
equal deleted inserted replaced
56406:0e21270952c3 56407:8e7ebc4b30f1