src/HOL/ex/Antiquote.thy
changeset 15172 73069e033a0b
parent 14981 e73f8140af78
child 16417 9bc16273c2d4