src/Pure/tactic.ML
changeset 26436 dfd6947ab5c2
parent 26424 a6cad32a27b0
child 26626 c6231d64d264