src/Pure/tactic.ML
changeset 48746 9e1b2aafbc7f
parent 46704 f800eb467515
child 49865 eeaf1ec7eac2