src/HOL/Complex/ex/BinEx.thy
changeset 28540 541366e3c1b3
parent 24075 366d4d234814
equal deleted inserted replaced
28539:bdb308737bfd 28540:541366e3c1b3