Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. make latex happy
  2. moved some theorems into HOL main corpus
  3. misc tuning and modernization
  4. more theorems for proof of concept for word type
  5. official fact collection sign_simps
  6. tuned proofs
  7. avoid pseudo-collection to be used in generated proofs
  8. moved comment to approproiate place
  9. removed outcommented example which seems not to work as advertized
  10. clear separation of types for bits (False / True) and Z2 (0 / 1)
  11. generalized type classes for parity to cover word types also, which contain zero divisors
  12. slightly more specialized name for type class
  13. dropped weaker legacy alias
  14. slightly more stringent ordering of theorems
  15. removed relics of ASCII syntax for indexed big operators
  16. dropped former legacy input abbreviations
  17. using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
  18. prefer fixed simpset for proof procedure
  19. tuned file system structure
  20. avoid spammed sledgehammer proofs
Changeset 70351:32b4e1aec5ca by haftmann:
make latex happy
The file was modified src/HOL/Library/Z2.thy (diff)
Changeset 70350:571ae57313a4 by haftmann:
moved some theorems into HOL main corpus
The file was modified src/HOL/Data_Structures/AVL_Set.thy (diff)
The file was modified src/HOL/Decision_Procs/Approximation_Bounds.thy (diff)
The file was modified src/HOL/Library/Log_Nat.thy (diff)
The file was modified src/HOL/Library/Tree_Real.thy (diff)
The file was modified src/HOL/Rat.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 70349:697450fd25c1 by haftmann:
misc tuning and modernization
The file was modified src/HOL/Library/Log_Nat.thy (diff)
Changeset 70348:bde161c740ca by haftmann:
more theorems for proof of concept for word type
The file was modified src/HOL/Library/Type_Length.thy (diff)
The file was modified src/HOL/ex/Word_Type.thy (diff)
Changeset 70347:e5cd5471c18a by haftmann:
official fact collection sign_simps
The file was modified NEWS (diff)
The file was modified src/HOL/Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Decision_Procs/Approximation_Bounds.thy (diff)
The file was modified src/HOL/Groups.thy (diff)
The file was modified src/HOL/Library/Float.thy (diff)
The file was modified src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy (diff)
The file was modified src/HOL/Rat.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
The file was modified src/HOL/ex/Ballot.thy (diff)
Changeset 70346:408e15cbd2a6 by haftmann:
tuned proofs
The file was modified src/HOL/Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Normed_Spaces.thy (diff)
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
Changeset 70345:80a1aa30e24d by haftmann:
avoid pseudo-collection to be used in generated proofs
The file was modified src/HOL/Rat.thy (diff)
Changeset 70344:050104f01bf9 by haftmann:
moved comment to approproiate place
The file was modified src/HOL/Fields.thy (diff)
The file was modified src/HOL/Rat.thy (diff)
Changeset 70343:e54caaa38ad9 by haftmann:
removed outcommented example which seems not to work as advertized
The file was modified src/HOL/Fields.thy (diff)
Changeset 70342:e4d626692640 by haftmann:
clear separation of types for bits (False / True) and Z2 (0 / 1)
The file was addedsrc/HOL/Library/Z2.thy
The file was addedsrc/HOL/Word/Bits_Z2.thy
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Word/Misc_Arithmetic.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)
The file was removedsrc/HOL/Library/Bit.thy
The file was removedsrc/HOL/Word/Bits_Bit.thy
Changeset 70341:972c0c744e7c by haftmann:
generalized type classes for parity to cover word types also, which contain zero divisors
The file was modified src/HOL/Groebner_Basis.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
The file was modified src/HOL/Presburger.thy (diff)
Changeset 70340:7383930fc946 by haftmann:
slightly more specialized name for type class
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/Groebner_Basis.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
The file was modified src/HOL/Presburger.thy (diff)
The file was modified src/HOL/Real_Asymp/Multiseries_Expansion.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/String.thy (diff)
The file was modified src/HOL/ex/Bit_Lists.thy (diff)
Changeset 70339:e939ea997f5f by haftmann:
dropped weaker legacy alias
The file was modified src/HOL/Parity.thy (diff)
The file was modified src/HOL/ex/Bit_Lists.thy (diff)
Changeset 70338:c832d431636b by haftmann:
slightly more stringent ordering of theorems
The file was modified src/HOL/Parity.thy (diff)
Changeset 70337:48609a6af1a0 by haftmann:
removed relics of ASCII syntax for indexed big operators
The file was modified NEWS (diff)
The file was modified src/HOL/Analysis/Abstract_Limits.thy (diff)
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Computational_Algebra/Formal_Laurent_Series.thy (diff)
Changeset 70336:559f45528804 by haftmann:
dropped former legacy input abbreviations
The file was modified src/HOL/Main.thy (diff)
Changeset 70335:9bd8c16b6627 by haftmann:
using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
The file was modified src/HOL/Library/Perm.thy (diff)
Changeset 70334:bba46912379e by haftmann:
prefer fixed simpset for proof procedure
The file was modified src/HOL/Library/Sum_of_Squares/sum_of_squares.ML (diff)
Changeset 70333:0f7edf0853df by haftmann:
tuned file system structure
The file was addedsrc/HOL/Library/Sum_of_Squares/positivstellensatz.ML
The file was modified src/HOL/Library/Sum_of_Squares.thy (diff)
The file was removedsrc/HOL/Library/positivstellensatz.ML
Changeset 70332:315489d836d8 by haftmann:
avoid spammed sledgehammer proofs
The file was modified src/HOL/Semiring_Normalization.thy (diff)