src/HOL/Complex/ex/BinEx.thy
changeset 28540 541366e3c1b3
parent 24075 366d4d234814