src/HOL/Complex.thy
changeset 54861 00d551179872
parent 54489 03ff4d1e6784
child 55734 3f5b2745d659