src/HOL/ex/Multiquote.thy
changeset 81434 1935ed4fe9c2
parent 80914 d97fdabd9e2b