#3998 (Oct 5, 2022, 9:50:02 AM)

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

1. remove temp file (detail)
2. Complex_Bounded_Operators: Various changes:
   
   - Removed auxiliary constant `the_riesz_rep_bilinear'`
   - Renamed constant `the_riesz_rep_bilinear` -> `the_riesz_rep_sesqui` and defined differently but equivalently
   - Renamed constant `bifunctional` -> `bidual_embedding`
     (and renamed lemmas containing `bifunctional` accordingly)
   - Renamed lemmas `the_riesz_rep_bilinear_apply` -> `the_riesz_rep_sesqui_apply`,
     `cblinfun_extension_exists_norm` -> `cblinfun_extension_norm_bounded_dense`
   - New theorems: `rank1_compose_left`, `rank1_compose_right`, `rank1_scaleC`,
     `rank1_uminus`, `rank1_uminus_iff`, `rank1_adj`, `rank1_adj_iff`,
     `bidual_embedding_surj`, `Cblinfun_comp_bounded_cbilinear`, `Cblinfun_comp_bounded_sesquilinear`, `bounded_clinear_0`,
     `bounded_antilinear_0`, `bounded_cbilinear_0`, `bounded_sesquilinear_0`, `bounded_cbilinear_apply_bounded_clinear`,
     `bounded_sesquilinear_apply_bounded_clinear`, `cblinfun_extension_exists_hilbert`,  `trunc_ell2_reduces_norm`,
     `trunc_ell2_add`, `trunc_ell2_scaleC`, `bounded_clinear_trunc_ell2`
   - Theorem `cblinfun_extension_exists_proj`: Reformulated one assumption (detail)

Started by an SCM change

This run spent:

• 2 min 0 sec waiting;
• 25 min build duration;
• 27 min total from scheduled to completion.