src/Pure/tactic.ML
changeset 26515 4a2063a8c2d2
parent 26424 a6cad32a27b0
child 26626 c6231d64d264