src/Pure/General/antiquote.ML
changeset 47815 43f677b3ae91
parent 45666 d83797ef0d2d
child 48764 4fe0920d5049
equal deleted inserted replaced
47814:53668571d300 47815:43f677b3ae91