src/HOL/Complex.thy
changeset 59445 2c27c3d1fd3b
parent 59000 6eb0725503fc
child 59613 7103019278f0