src/Pure/tactic.ML
changeset 33841 6508d0e8bb19
parent 32971 55ba9b6648ef
child 33955 fff6f11b1f09
equal deleted inserted replaced
33840:f00a8956d6d0 33841:6508d0e8bb19