Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned
  2. simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
  3. dropped redundant syntax translation rules for big operators
  4. moved lemma from AFP
  5. tuned lemmas
  6. merged
  7. tuned
Changeset 68797:e79c771c0619 by haftmann:
tuned
The file was modified src/HOL/Complete_Lattices.thy (diff)
Changeset 68796:9ca183045102 by haftmann:
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
The file was modified NEWS (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/Lattices_Big.thy (diff)
Changeset 68795:210b687cdbbe by haftmann:
dropped redundant syntax translation rules for big operators
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/Lattices_Big.thy (diff)
Changeset 68794:63e84bd8e1f6 by nipkow:
moved lemma from AFP
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
Changeset 68793:462226db648a by nipkow:
tuned lemmas
The file was modified src/HOL/Lattices_Big.thy (diff)
Changeset 68792:d2470f3a768b by nipkow:
merged
Changeset 68791:5e7b3e6625eb by nipkow:
tuned
The file was modified src/Doc/Prog_Prove/document/intro-isabelle.tex (diff)