src/HOL/IMPP/Misc.thy
changeset 40117 ea388cb9bc57
parent 28524 644b62cf678f
child 41589 bbd861837ebc