src/Pure/tactic.ML
changeset 20815 ccf18b899c8d
parent 20302 265b2342cf21
child 21687 f689f729afab