src/Pure/tactic.ML
changeset 27930 2b44df907cc2
parent 27243 d549b5b0f344
child 29276 94b1ffec9201