src/HOL/Library/Power_By_Squaring.thy
changeset 80680 d517afba4968
parent 69790 154cf64e403e