src/HOL/IMPP/Misc.thy
changeset 28965 1de908189869
parent 28524 644b62cf678f
child 41589 bbd861837ebc