src/HOL/Complex.thy
changeset 37497 71fdbffe3275
parent 36825 d9320cdcde73
child 37767 a2b7a20d6ea3