src/HOL/Complex/ex/BinEx.thy
changeset 17836 5d9c9e284d16
parent 15149 c5c4884634b7
child 23477 f4b83f03cac9
equal deleted inserted replaced
17835:74e6140e5f1f 17836:5d9c9e284d16