src/HOL/Power.thy
changeset 18937 0eb35519f0f3
parent 17149 e2b19c92ef51
child 21199 2d83f93c3580