src/HOL/Complex_Main.thy
changeset 81271 fb391ad09b3c
parent 80177 1478555580af
equal deleted inserted replaced
81270:b98595f82a88 81271:fb391ad09b3c