Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div
  2. dropped tautological pattern
  3. more warning comments
  4. more lemmas
  5. spelling
Changeset 63950:cdc1e59aa513 by haftmann:
syntactic type class for operation mod named after mod;<br>simplified assumptions of type class semiring_div
The file was modified NEWS (diff)
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/Doc/Tutorial/Misc/appendix.thy (diff)
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/Enum.thy (diff)
The file was modified src/HOL/Import/HOL_Light_Maps.thy (diff)
The file was modified src/HOL/Library/Old_SMT/old_smt_normalize.ML (diff)
The file was modified src/HOL/Library/Old_SMT/old_z3_interface.ML (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/Library/Predicate_Compile_Alternative_Defs.thy (diff)
The file was modified src/HOL/Mutabelle/mutabelle_extra.ML (diff)
The file was modified src/HOL/Nonstandard_Analysis/StarDef.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
The file was modified src/HOL/SMT_Examples/SMT_Examples.certs (diff)
The file was modified src/HOL/SPARK/Tools/spark_vcs.ML (diff)
The file was modified src/HOL/String.thy (diff)
The file was modified src/HOL/Tools/Qelim/cooper.ML (diff)
The file was modified src/HOL/Tools/SMT/z3_interface.ML (diff)
The file was modified src/HOL/Tools/lin_arith.ML (diff)
The file was modified src/HOL/Tools/numeral_simprocs.ML (diff)
The file was modified src/HOL/Word/Word.thy (diff)
The file was modified src/HOL/ex/Arith_Examples.thy (diff)
Changeset 63949:e7e41db7221b by haftmann:
dropped tautological pattern
The file was modified src/HOL/Tools/lin_arith.ML (diff)
Changeset 63948:429cfc5f2559 by haftmann:
more warning comments
The file was modified src/HOL/Tools/lin_arith.ML (diff)
Changeset 63947:559f0882d6a6 by haftmann:
more lemmas
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
Changeset 63946:d05da6b707dd by haftmann:
spelling
The file was modified NEWS (diff)