Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. prefer constructive primitive_part over implicit content_decompose
  2. merged
  3. tuned lemmas
  4. more uniform parameter naming convention for choose and gchoose
  5. slightly generalized theorems
  6. tuned code setup
  7. tuned
  8. more theorems on fact
  9. removed ineffective code equation
  10. tuned whitespace
  11. new simp rule
  12. copied but not adapted
Changeset 68790:851a9d9746c6 by haftmann:
prefer constructive primitive_part over implicit content_decompose
The file was modified src/HOL/Computational_Algebra/Polynomial.thy (diff)
The file was modified src/HOL/Computational_Algebra/Polynomial_Factorial.thy (diff)
Changeset 68789:9270af426282 by nipkow:
merged
Changeset 68788:d4426a23832e by nipkow:
tuned lemmas
The file was modified src/HOL/Lattices_Big.thy (diff)
Changeset 68787:b129052644e9 by haftmann:
more uniform parameter naming convention for choose and gchoose
The file was modified src/HOL/Binomial.thy (diff)
Changeset 68786:134be95e5787 by haftmann:
slightly generalized theorems
The file was modified src/HOL/Binomial.thy (diff)
Changeset 68785:862b1288020f by haftmann:
tuned code setup
The file was modified src/HOL/Binomial.thy (diff)
Changeset 68784:c7ee984243fc by haftmann:
tuned
The file was modified src/HOL/Binomial.thy (diff)
Changeset 68783:248e1678ce55 by haftmann:
more theorems on fact
The file was modified src/HOL/Factorial.thy (diff)
Changeset 68782:8ff34c1ad580 by haftmann:
removed ineffective code equation
The file was modified src/HOL/Library/Mapping.thy (diff)
Changeset 68781:567079abb173 by haftmann:
tuned whitespace
The file was modified src/HOL/List.thy (diff)
Changeset 68780:54fdc8bc73a3 by haftmann:
new simp rule
The file was modified src/HOL/HOLCF/Cont.thy (diff)
The file was modified src/HOL/HOLCF/Library/List_Cpo.thy (diff)
The file was modified src/HOL/HOLCF/Porder.thy (diff)
The file was modified src/HOL/HOLCF/Universal.thy (diff)
The file was modified src/HOL/Set.thy (diff)
Changeset 68779:78d9b1783378 by nipkow:
copied but not adapted
The file was modified src/HOL/Lattices_Big.thy (diff)