[isabelle-dev] NEWS (constant ii)

Lawrence Paulson lp15 at cam.ac.uk
Tue Feb 28 14:58:07 CET 2017


* Renamed ii to imaginary_unit in order to free up ii as a variable name. 
The syntax \<i> remains available.
INCOMPATIBILITY.

To my surprise, there are thousands of occurrences of ii throughout the library than the AFP. The overwhelming majority of these have nothing to do with the complex numbers. Therefore it is highly likely that I have overlooked a few that are. But anyway, the repository builds.

Larry



More information about the isabelle-dev mailing list