Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. remove trailing whitespaces in List
  2. drop a superfluous assumption that was found by the find_unused_assms command
  3. drop a superfluous assumption that was found by the find_unused_assms command and tune proof
  4. drop a superfluous assumption that was found by the find_unused_assms command and tune proof
  5. algebraic foundation for congruences
Changeset 66892:d67d28254ff2 by bulwahn:
remove trailing whitespaces in List
The file was modified src/HOL/List.thy (diff)
Changeset 66891:5ec8cd4db7e2 by bulwahn:
drop a superfluous assumption that was found by the find_unused_assms command
The file was modified src/HOL/List.thy (diff)
Changeset 66890:e92d48a42a01 by bulwahn:
drop a superfluous assumption that was found by the find_unused_assms command and tune proof
The file was modified src/HOL/List.thy (diff)
Changeset 66889:7fe528893a6c by bulwahn:
drop a superfluous assumption that was found by the find_unused_assms command and tune proof
The file was modified src/HOL/List.thy (diff)
Changeset 66888:930abfdf8727 by haftmann:
algebraic foundation for congruences
The file was modified src/HOL/Number_Theory/Cong.thy (diff)
The file was modified src/HOL/Number_Theory/Euler_Criterion.thy (diff)
The file was modified src/HOL/Number_Theory/Gauss.thy (diff)
The file was modified src/HOL/Number_Theory/Pocklington.thy (diff)
The file was modified src/HOL/Number_Theory/Quadratic_Reciprocity.thy (diff)
The file was modified src/HOL/Number_Theory/Residues.thy (diff)
The file was modified src/HOL/Number_Theory/Totient.thy (diff)