src/Pure/tactic.ML
changeset 4962 e9217cb15b42
parent 4713 bea2ab2e360b
child 5263 8862ed2db431