src/HOL/Complex.thy
changeset 30840 98809b3f5e3c
parent 30729 461ee3e49ad3
child 30960 fec1a04b7220