HomeIsabelle/Phabricator
Diffusion afp-devel c4c97fa55b33

Complex_Bounded_Operators: update to isabelle@ffb15f7f26d5
c4c97fa55b33
Actions

Description

Complex_Bounded_Operators: update to isabelle@ffb15f7f26d5

Details

Provenance
kleingAuthored on
Parents
rAFP91a58b10dae0: Weighted_Path_Order: update to isabelle@ffb15f7f26d5
Branches
Unknown
Tags
Unknown

Changes (12)

PathSize
thys/
Complex_Bounded_Operators/
extra/

rAFPc4c97fa55b33

View Options

thys/Complex_Bounded_Operators/Cblinfun_Matrix.thy

Loading...
View Options

thys/Complex_Bounded_Operators/Complex_Bounded_Linear_Function.thy

Loading...
View Options

thys/Complex_Bounded_Operators/Complex_Inner_Product.thy

Loading...
View Options

thys/Complex_Bounded_Operators/Complex_Inner_Product0.thy

Loading...
View Options

thys/Complex_Bounded_Operators/Complex_Vector_Spaces.thy

Loading...
View Options

thys/Complex_Bounded_Operators/Complex_Vector_Spaces0.thy

Loading...
View Options

thys/Complex_Bounded_Operators/ROOT

Loading...
View Options

thys/Complex_Bounded_Operators/extra/Extra_Infinite_Set_Sum.thy

Loading...
View Options

thys/Complex_Bounded_Operators/extra/Extra_Lattice.thy

Loading...
View Options

thys/Complex_Bounded_Operators/extra/Extra_Operator_Norm.thy

Loading...
View Options

thys/Complex_Bounded_Operators/extra/Extra_Ordered_Fields.thy

Loading...
View Options

thys/Complex_Bounded_Operators/extra/Extra_Pretty_Code_Examples.thy

Loading...