src/Pure/tactic.ML
changeset 27963 c9ea82444189
parent 27243 d549b5b0f344
child 29276 94b1ffec9201