src/HOL/Library/Power_By_Squaring.thy
changeset 82633 38f5ecbb4574
parent 69790 154cf64e403e