* 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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to