src/Pure/tactic.ML
changeset 4003 2bbeed529077
parent 3991 4cb2f2422695
child 4178 e64ff1c1bc70