Changes

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Changeset 14311:22721115789f by Dominique Unruh _hg.yse9he@rwth.unruh.de_: Miscellaneous changes to Complex_Bounded_Operators.
The file was modified	`thys/Complex_Bounded_Operators/Complex_Bounded_Linear_Function.thy`
The file was modified	`thys/Complex_Bounded_Operators/Complex_Inner_Product.thy`
The file was modified	`thys/Complex_Bounded_Operators/Complex_Inner_Product0.thy`
The file was modified	`thys/Complex_Bounded_Operators/Complex_L2.thy`
The file was modified	`thys/Complex_Bounded_Operators/Complex_Vector_Spaces.thy`
The file was modified	`thys/Complex_Bounded_Operators/One_Dimensional_Spaces.thy`
The file was modified	`thys/Complex_Bounded_Operators/extra/Extra_Ordered_Fields.thy`
The file was modified	`thys/Complex_Bounded_Operators/extra/Extra_Vector_Spaces.thy`