src/HOL/ex/Antiquote.thy
changeset 10434 6ea4735c3955
parent 10357 0d0cac129618
child 11586 d8a7f6318457