src/HOL/Complex.thy
changeset 78907 89274adb0ebe
parent 78698 1b9388e6eb75
child 80932 261cd8722677
equal deleted inserted replaced
78906:004b39bf06a5 78907:89274adb0ebe