Summary
- merge
- added three theory files, for signed multisets and friends
- 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 added | thys/Nested_Multisets_Ordinals/Signed_Hereditary_Multiset.thy |
The file was added | thys/Nested_Multisets_Ordinals/Signed_Multiset.thy |
The file was added | thys/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) |
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) |