Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. generalize more theorems to support enat and ennreal
  2. moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
  3. Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
  4. add extended nonnegative real numbers
  5. remove lattice syntax from countable complete lattice
  6. add countable complete lattices
  7. Borel_Space.borel is now in the type class locale
  8. add tendsto_add_ereal_nonneg
  9. add transfer rule for countable
  10. instantiate topologies for nat, int and enat
  11. add type class for topological monoids
  12. move product topology to HOL-Complex_Main
Changeset 62378:85ed00c1fe7c by hoelzl:
generalize more theorems to support enat and ennreal
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/Decision_Procs/Polynomial_List.thy (diff)
The file was modified src/HOL/Filter.thy (diff)
The file was modified src/HOL/Groups.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/IMP/Abs_Int_ITP/Abs_Int1_ITP.thy (diff)
The file was modified src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy (diff)
The file was modified src/HOL/Library/Extended_Nat.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/NSA/HyperNat.thy (diff)
The file was modified src/HOL/NSA/StarDef.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/Quotient_Examples/Int_Pow.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
Changeset 62377:ace69956d018 by hoelzl:
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
The file was modified src/HOL/Groups.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
The file was modified src/HOL/Series.thy (diff)
Changeset 62376:85f38d5f8807 by hoelzl:
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
The file was modified NEWS (diff)
The file was modified src/HOL/Groups.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/Library/Convex.thy (diff)
The file was modified src/HOL/Library/Extended_Nat.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Library/Function_Algebras.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy (diff)
The file was modified src/HOL/NSA/StarDef.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
The file was modified src/HOL/Series.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
Changeset 62375:670063003ad3 by hoelzl:
add extended nonnegative real numbers
The file was addedsrc/HOL/Library/Extended_Nonnegative_Real.thy
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy (diff)
The file was modified src/HOL/Probability/Weak_Convergence.thy (diff)
Changeset 62374:cb27a55d868a by hoelzl:
remove lattice syntax from countable complete lattice
The file was modified src/HOL/Library/Countable_Complete_Lattices.thy (diff)
The file was modified src/HOL/Library/Extended_Nat.thy (diff)
The file was modified src/HOL/Library/Order_Continuity.thy (diff)
Changeset 62373:ea7a442e9a56 by hoelzl:
add countable complete lattices
The file was addedsrc/HOL/Library/Countable_Complete_Lattices.thy
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Library/Order_Continuity.thy (diff)
Changeset 62372:4fe872ff91bf by hoelzl:
Borel_Space.borel is now in the type class locale
The file was modified src/HOL/Library/Countable_Set_Type.thy (diff)
The file was modified src/HOL/Probability/Borel_Space.thy (diff)
Changeset 62371:7c288c0c7300 by hoelzl:
add tendsto_add_ereal_nonneg
The file was modified src/HOL/Library/Extended_Real.thy (diff)
Changeset 62370:4a35e3945cab by hoelzl:
add transfer rule for countable
The file was modified src/HOL/Library/Countable_Set.thy (diff)
Changeset 62369:acfc4ad7b76a by hoelzl:
instantiate topologies for nat, int and enat
The file was modified src/HOL/Filter.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
Changeset 62368:106569399cd6 by hoelzl:
add type class for topological monoids
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Series.thy (diff)
Changeset 62367:d2bc8a7e5fec by hoelzl:
move product topology to HOL-Complex_Main
The file was modified src/HOL/Filter.thy (diff)
The file was modified src/HOL/Library/Product_Vector.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)