legacy_Complex_simps

[Makarius]

On 04/04/2025 13:06, Lawrence Paulson via isabelle-dev wrote:
> Can anybody explain why all of the lemmas about the complex constructor “Complex" have been shoved into this lemma list, legacy_Complex_simps?
> 
> There is seemingly a view to push users into writing complex expressions in the form x + iy, which looks nice in a mathematics textbook but is certain to complicate reasoning where the real and imaginary parts are dealt with separately.

The Isabelle sources follow the principle that "the history is the proof for 
the state of the text". Here is the relevant changeset from 07-May-2014 by 
Johannes Hölzl: https://isabelle-dev.sketis.net/rISABELLE48a745e1bde7

Maybe you can make sense from that.


	Makarius