src/HOL/ex/Antiquote.thy
changeset 7843 077d305615df
parent 5368 7c8d1c7c876d
child 8559 fd3753188232
equal deleted inserted replaced
7842:6858c98385c3 7843:077d305615df