src/Pure/tctical.ML
changeset 4666 b7c4e4ade1aa
parent 4602 0e034d76932e
child 5141 495a4f9af897