Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. adjusted proofs
  3. added and reorganized lemmas (some suggested by Jeremy Sylvestre)
  4. removed redundant lemma
  5. moved theorem from Fun to Set
  6. added lemmas antisymp_ge[simp], antisymp_greater[simp], antisymp_le[simp], and antisymp_less[simp]
  7. added lemmas reflp_ge[simp] and reflp_le[simp]
Changeset 76263:5ede2fce5b01 by nipkow:
merged
Changeset 76262:7aa2eb860db4 by nipkow:
adjusted proofs
The file was modified src/HOL/Number_Theory/Gauss.thy (diff)
Changeset 76261:26524d0b4395 by nipkow:
added and reorganized lemmas (some suggested by Jeremy Sylvestre)
The file was modified src/HOL/Fun.thy (diff)
Changeset 76260:5fd8ba24ca48 by nipkow:
removed redundant lemma
The file was modified src/HOL/Fun.thy (diff)
Changeset 76259:d1c26efb7a47 by nipkow:
moved theorem from Fun to Set
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Set.thy (diff)
Changeset 76258:2f10e7a2ff01 by desharna:
added lemmas antisymp_ge[simp], antisymp_greater[simp], antisymp_le[simp], and antisymp_less[simp]
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 76257:61a5b5ad3a6e by desharna:
added lemmas reflp_ge[simp] and reflp_le[simp]
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)