src/Pure/tactic.ML
changeset 59456 180555df34ea
parent 59164 ff40c53d1af9
child 59498 50b60f501b05