src/Pure/tactic.ML
changeset 10168 50be659d4222
parent 9535 a60b0be5ee96
child 10347 c0cfc4ac12e2