Diffusion afp-devel d23129e35a65

Complex_Bounded_Operators: Fixed document generation
d23129e35a65
Actions

Tags

None

Subscribers

None

Description

Complex_Bounded_Operators: Fixed document generation

Details

Provenance

Dominique Unruh <unruh@ut.ee>

Authored on

Parents

rAFPec167025ccd6: Merged changes.

Branches

Unknown

Tags

Unknown

Event Timeline

Dominique Unruh <unruh@ut.ee> committed rAFPd23129e35a65: Complex_Bounded_Operators: Fixed document generation.Aug 23 2022, 9:44 PM

Changes (2)

Path

Size

thys/

Complex_Bounded_Operators/

Complex_Vector_Spaces.thy

extra/

Extra_General.thy

rAFPd23129e35a65

thys/Complex_Bounded_Operators/Complex_Vector_Spaces.thy

Loading...

thys/Complex_Bounded_Operators/extra/Extra_General.thy

Loading...