src/HOL/IMPP/Misc.thy
changeset 39159 0dec18004e75
parent 28524 644b62cf678f
child 41589 bbd861837ebc