src/Pure/tactic.ML
changeset 6903 682f8a9ec75d
parent 6390 5d58c100ca3f
child 6964 0c894ad53457