src/HOL/Power.thy
changeset 27479 9bcd25618d0c
parent 25874 14819a95cf75
child 28131 3130d7b3149d