src/HOL/ex/Antiquote.thy
changeset 9165 f46f407080f8
parent 8559 fd3753188232
child 9297 bafe45732b10