src/Pure/tactic.ML
changeset 29270 0eade173f77e
parent 27243 d549b5b0f344
child 29276 94b1ffec9201