src/Pure/tactic.ML
changeset 9841 ca3173f87b5c
parent 9535 a60b0be5ee96
child 10347 c0cfc4ac12e2