Summary
- Ergodic_Theory: moved Product_Topology to Isabelle; Lp: moved Essential Supremum to Isabelle
- renamed convergent_eq_cauchy
The file was modified | thys/Ergodic_Theory/Measure_Preserving_Transformations.thy (diff) |
The file was modified | thys/Ergodic_Theory/ROOT (diff) |
The file was modified | thys/Ergodic_Theory/SG_Library_Complement.thy (diff) |
The file was modified | thys/Lp/Lp.thy (diff) |
The file was removed | thys/Ergodic_Theory/Product_Topology.thy |
The file was modified | thys/Lp/Functional_Spaces.thy (diff) |