src/HOL/Complex/ex/BinEx.thy
changeset 25656 7f4cf5b20d38
parent 24075 366d4d234814