src/Pure/tactic.ML
changeset 1868 836950047d85
parent 1801 927a31ba4346
child 1951 f2b8005bdc6e