src/Pure/tactic.ML
changeset 21405 26b51f724fe6
parent 20302 265b2342cf21
child 21687 f689f729afab