src/Pure/tactic.ML
changeset 6930 4b40fb299f9f
parent 6390 5d58c100ca3f
child 6964 0c894ad53457