src/Pure/tactic.ML
changeset 21404 eb85850d3eb7
parent 20302 265b2342cf21
child 21687 f689f729afab