Imported a theorem about Infinite_Sum. Importing this theory a bit earlier is causing syntactic ambiguities with Infinite_Set_Sum however; no_notation needed
Description
Description
Details
Details
- Provenance
paulson <lp15@cam.ac.uk> Authored on - Parents
- rISABELLE8fe30123aaab: merged
- Branches
- Unknown
- Tags