Skip to content
Failed

Changes

Summary

  1. merge
  2. added three theory files, for signed multisets and friends
  3. Deep_Learning: ereal -> ennreal; add missing type class instance poly_mapping :: ordered_cancel_comm_monoid_add (otherwise mpoly::ring_no_divisors fails)
Changeset 7412:d2636de14fc1 by blanchet:
merge
Changeset 7411:d3e49dec051b by blanchet:
added three theory files, for signed multisets and friends
The file was addedthys/Nested_Multisets_Ordinals/Signed_Hereditary_Multiset.thy
The file was addedthys/Nested_Multisets_Ordinals/Signed_Multiset.thy
The file was addedthys/Nested_Multisets_Ordinals/Signed_Syntactic_Ordinal.thy
The file was modified thys/Nested_Multisets_Ordinals/Hereditary_Multiset.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/README (diff)
The file was modified thys/Nested_Multisets_Ordinals/ROOT (diff)
The file was modified thys/Nested_Multisets_Ordinals/document/root.tex (diff)
Changeset 7410:34f5bdc3bb0a by hoelzl:
Deep_Learning: ereal -> ennreal; add missing type class instance poly_mapping :: ordered_cancel_comm_monoid_add (otherwise mpoly::ring_no_divisors fails)
The file was modified thys/Deep_Learning/DL_Fundamental_Theorem_Network_Capacity.thy (diff)
The file was modified thys/Deep_Learning/Lebesgue_Zero_Set.thy (diff)
The file was modified thys/Deep_Learning/PP_MPoly.thy (diff)
The file was modified thys/Deep_Learning/PP_Poly_Mapping.thy (diff)