src/Pure/tactic.ML
changeset 16885 cabcd33cde18
parent 16876 f57b38cced32
child 16942 c01816b32c04