Started 4 hr 6 min ago
Build has been executing for 4 hr 6 min on workerlrz5

Build #2084 (Oct 4, 2022, 1:33:11 AM)
Progress:

Changes

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

  1. Many changes to entry `Complex_Bounded_Operators`:
    - Removed all use of deprecated `⟨.,.⟩` syntax for complex inner product. (Now: `∙⇩C`)
    - Cosmetic changes and cleanup of some proofs
    - Type class `one_dim` inherits from `complex_inner` now.
    - Moved various theorems around between theories
    - Added `[simp]` to: `Proj_partial_isometry`, `cadjoint_id`
    - Removed theorems: `onorm_Inf_bound`, `norm_unit_sphere`
    - Changed theorems: `of_complex_cblinfun_apply` (made into more general simp-rule), TODO orthospacething
    - New definition: `rank1` (and lemmas about it)
    - New theorems: `one_dim_iso_cblinfun_apply`, `vector_to_cblinfun_one_dim_iso`, `image_vector_to_cblinfun_adj`,
      `image_vector_to_cblinfun_adj'`, `sgn_cinner`, `orthocomplement_top`, `orthogonal_spaces_ccspan`, `norm_scaleC_sgn`,
      `one_dim_ccsubspace_all_or_nothing`, `surj_isometry_is_unitary`
    - Renamed `vector_to_cblinfun_cblinfun_apply` -> `vector_to_cblinfun_cblinfun_compose` (also turned around and added `[simp]`),
      `cancel_apply_Proj` -> `Proj_fixes_image`, `range_is_clinear` -> `range_is_csubspace`.
    - Changed definition: `is_Proj` (logically equivalent by `Proj_range_closed`)

    Fixed entry `Registers` due to the changes above. (detail)

Started by an SCM change

This run spent 9.7 sec waiting in the queue.

Revision: 6ab4bb7cb8b2cb6d85c564b75fa29cef0aace417
Revision: 1145c2ed8f6c99ebd9c6711a59f3a4d226c9bfbb