Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. fix problems because of "surj" input abbreviation; tuned
  3. hide global sum
  4. gcd/lcm on finite sets
  5. moved some lemmas to appropriate places
  6. slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
Changeset 64853:9178214b3588 by nipkow:
merged
Changeset 64852:f3504bc69ea3 by nipkow:
fix problems because of "surj" input abbreviation; tuned
The file was modified src/Doc/Prog_Prove/Isar.thy (diff)
The file was modified src/Doc/Prog_Prove/document/intro-isabelle.tex (diff)
Changeset 64851:33aab75ff423 by nipkow:
hide global sum
The file was modified src/HOL/IMP/Hoare_Examples.thy (diff)
Changeset 64850:fc9265882329 by haftmann:
gcd/lcm on finite sets
The file was modified src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/Library/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff)
Changeset 64849:766db3539859 by haftmann:
moved some lemmas to appropriate places
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/Library/Polynomial.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/Rat.thy (diff)
Changeset 64848:c50db2128048 by haftmann:
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/Library/Polynomial.thy (diff)
The file was modified src/HOL/Library/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff)
The file was modified src/HOL/Rings.thy (diff)