src/Pure/tactic.ML
changeset 12021 8809efda06d3
parent 11974 f76c3e1ab352
child 12139 d51d50636332