src/Pure/General/antiquote.ML
changeset 60988 1d7a7e33fd67
parent 59112 e670969f34df
child 61434 46d6586eb04c
equal deleted inserted replaced
60987:ea00d17eba3b 60988:1d7a7e33fd67