src/Pure/type_infer.ML
changeset 20205 7b2958d3d575
parent 20161 b8b1d4a380aa
child 20668 00521d5e1838