src/Pure/Tools/am_interpreter.ML
changeset 19532 dae447f2b0b4
parent 17795 5b18c3343028
equal deleted inserted replaced
19531:89970e06351f 19532:dae447f2b0b4