src/HOL/IMPP/Misc.thy
changeset 41101 c1d1ec5b90f1
parent 28524 644b62cf678f
child 41589 bbd861837ebc