src/Pure/tactic.ML
changeset 33205 20587741a8d9
parent 32971 55ba9b6648ef
child 33955 fff6f11b1f09