src/HOL/ex/Multiquote.thy
changeset 8765 1bc30ff5fc54
parent 8627 44ec33bb5c5b
child 9297 bafe45732b10
equal deleted inserted replaced
8764:3f976a7e81d3 8765:1bc30ff5fc54