src/HOL/Complex/ex/BinEx.thy
changeset 14467 bbfa6b01a55f
parent 14373 67a628beb981
child 15149 c5c4884634b7