Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. brought back [...] maplet syntax
  2. merged
  3. has_sum now an infix operator!!
  4. merged
  5. New material contributed by Manuel
  6. Map.empty no longer output abbreviation; %_. None is shorter and requires no explanation
Changeset 77361:b34435f2a2bf by nipkow:
brought back [...] maplet syntax
The file was modified src/HOL/Map.thy (diff)
Changeset 77360:ef03267af5a7 by paulson:
merged
Changeset 77359:bfb1acc9855e by paulson _lp15@cam.ac.uk_:
has_sum now an infix operator!!
The file was modified src/HOL/Analysis/Infinite_Sum.thy (diff)
Changeset 77358:4a0b0cf9e4d0 by paulson:
merged
Changeset 77357:e65d8ee80811 by paulson _lp15@cam.ac.uk_:
New material contributed by Manuel
The file was modified src/HOL/Analysis/Infinite_Sum.thy (diff)
Changeset 77356:1f5428d66591 by nipkow:
Map.empty no longer output abbreviation; %_. None is shorter and requires no explanation
The file was modified NEWS (diff)
The file was modified src/HOL/Map.thy (diff)