src/HOL/Complex.thy
changeset 36817 ed97e877ff2d
parent 36777 be5461582d0f
child 36825 d9320cdcde73