src/Pure/tactic.ML
changeset 5997 4d00bbd3d3ac
parent 5974 6acf3ff0f486
child 6390 5d58c100ca3f