src/Pure/tactic.ML
changeset 59248 167c2ebdfab4
parent 59164 ff40c53d1af9
child 59498 50b60f501b05