src/Pure/tactical.ML
changeset 59804 db0b87085c16
parent 59660 49e498cedd02
child 60941 e7c761c63c18