src/Pure/General/scan.ML
changeset 56202 0a11d17eeeff
parent 55104 8284c0d5bf52
child 58850 1bb0ad7827b4
equal deleted inserted replaced
56201:dd2df97b379b 56202:0a11d17eeeff