Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. special treatment of 0 only refers to type char
  2. merged
  3. features and caveats of datatype_record
  4. merged
  5. strengthen filter relator to canonical categorical definition with better properties
Changeset 67620:3817a93a3e5e by haftmann:
special treatment of 0 only refers to type char
The file was modified src/HOL/Tools/string_code.ML (diff)
Changeset 67619:37ba3d234fbf by lars hupel _lars.hupel@mytum.de_:
merged
Changeset 67618:3107dcea3493 by lars hupel _lars.hupel@mytum.de_:
features and caveats of datatype_record
The file was modified src/HOL/Library/Datatype_Records.thy (diff)
Changeset 67617:9f9f64fe1705 by Andreas Lochbihler:
merged
Changeset 67616:1d005f514417 by Andreas Lochbihler:
strengthen filter relator to canonical categorical definition with better properties
The file was modified NEWS (diff)
The file was modified src/HOL/Filter.thy (diff)