src/HOL/ex/Multiquote.thy
changeset 8765 1bc30ff5fc54
parent 8627 44ec33bb5c5b
child 9297 bafe45732b10