Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. reoriented congruence rules in non-explosive direction
  2. more fine-grained type class hierarchy for div and mod
  3. restructured matter on polynomials and normalized fractions
  4. streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
  5. tuned fact references
  6. clarified library contents
  7. standardized notation
  8. redundant
  9. renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
  10. added lemmas demanded by FIXMEs
  11. dropped comment after conversation with author: predicate compiler works independently from any code generator setup
Changeset 64593:50c715579715 by haftmann:
reoriented congruence rules in non-explosive direction
The file was modified NEWS (diff)
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Decision_Procs/cooper_tac.ML (diff)
The file was modified src/HOL/Decision_Procs/mir_tac.ML (diff)
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/Groebner_Basis.thy (diff)
The file was modified src/HOL/IMP/Abs_Int1_parity.thy (diff)
The file was modified src/HOL/Library/Numeral_Type.thy (diff)
The file was modified src/HOL/Library/Omega_Words_Fun.thy (diff)
The file was modified src/HOL/Number_Theory/Cong.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/SPARK/Examples/RIPEMD-160/Round.thy (diff)
The file was modified src/HOL/SPARK/Manual/Proc1.thy (diff)
The file was modified src/HOL/SPARK/Manual/Proc2.thy (diff)
The file was modified src/HOL/Tools/Qelim/cooper.ML (diff)
The file was modified src/HOL/Word/Bit_Representation.thy (diff)
The file was modified src/HOL/Word/Bits_Int.thy (diff)
The file was modified src/HOL/Word/Misc_Numeric.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)
The file was modified src/HOL/Word/Word_Miscellaneous.thy (diff)
The file was modified src/HOL/ex/Word_Type.thy (diff)
Changeset 64592:7759f1766189 by haftmann:
more fine-grained type class hierarchy for div and mod
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/Library/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Library/Normalized_Fraction.thy (diff)
The file was modified src/HOL/Library/Polynomial.thy (diff)
The file was modified src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
Changeset 64591:240a39af9ec4 by haftmann:
restructured matter on polynomials and normalized fractions
The file was addedsrc/HOL/Library/Field_as_Ring.thy
The file was modified src/HOL/Fields.thy (diff)
The file was modified src/HOL/Fun_Def.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Normalized_Fraction.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/ROOT (diff)
The file was modified src/HOL/Rings.thy (diff)
Changeset 64590:6621d91d3c8a by haftmann:
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
The file was modified src/HOL/Number_Theory/Primes.thy (diff)
Changeset 64589:c1932a4a227f by haftmann:
tuned fact references
The file was modified src/HOL/Tools/Qelim/cooper.ML (diff)
Changeset 64588:293ab573d034 by haftmann:
clarified library contents
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 64587:8355a6e2df79 by haftmann:
standardized notation
The file was modified src/HOL/Algebra/Coset.thy (diff)
The file was modified src/HOL/Algebra/Divisibility.thy (diff)
The file was modified src/HOL/Library/DAList_Multiset.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Multiset_Order.thy (diff)
The file was modified src/HOL/Library/Permutation.thy (diff)
Changeset 64586:1d25ca718790 by haftmann:
redundant
The file was modified src/HOL/Library/Multiset.thy (diff)
Changeset 64585:2155c0c1ecb6 by haftmann:
renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
The file was modified src/HOL/Library/Multiset.thy (diff)
Changeset 64584:142ac30b68fe by haftmann:
added lemmas demanded by FIXMEs
The file was modified src/HOL/Relation.thy (diff)
Changeset 64583:2edac4e13918 by haftmann:
dropped comment after conversation with author: predicate compiler works independently from any code generator setup
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML (diff)