src/HOL/Power.thy
changeset 8115 c802042066e8
parent 7843 077d305615df
child 8844 db71c334e854