SuccessChanges

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 70536:32b4e1aec5ca by haftmann:
make latex happy
The file was modifiedsrc/HOL/Library/Z2.thy (diff)
Changeset 70535:571ae57313a4 by haftmann:
moved some theorems into HOL main corpus
The file was modifiedsrc/HOL/Data_Structures/AVL_Set.thy (diff)
The file was modifiedsrc/HOL/Decision_Procs/Approximation_Bounds.thy (diff)
The file was modifiedsrc/HOL/Library/Log_Nat.thy (diff)
The file was modifiedsrc/HOL/Library/Tree_Real.thy (diff)
The file was modifiedsrc/HOL/Rat.thy (diff)
The file was modifiedsrc/HOL/Transcendental.thy (diff)
Changeset 70534:697450fd25c1 by haftmann:
misc tuning and modernization
The file was modifiedsrc/HOL/Library/Log_Nat.thy (diff)
Changeset 70533:bde161c740ca by haftmann:
more theorems for proof of concept for word type
The file was modifiedsrc/HOL/Library/Type_Length.thy (diff)
The file was modifiedsrc/HOL/ex/Word_Type.thy (diff)
Changeset 70532:e5cd5471c18a by haftmann:
official fact collection sign_simps
The file was modifiedNEWS (diff)
The file was modifiedsrc/HOL/Analysis/Conformal_Mappings.thy (diff)
The file was modifiedsrc/HOL/Decision_Procs/Approximation_Bounds.thy (diff)
The file was modifiedsrc/HOL/Groups.thy (diff)
The file was modifiedsrc/HOL/Library/Float.thy (diff)
The file was modifiedsrc/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy (diff)
The file was modifiedsrc/HOL/Rat.thy (diff)
The file was modifiedsrc/HOL/Rings.thy (diff)
The file was modifiedsrc/HOL/ex/Ballot.thy (diff)
Changeset 70531:408e15cbd2a6 by haftmann:
tuned proofs
The file was modifiedsrc/HOL/Analysis/Conformal_Mappings.thy (diff)
The file was modifiedsrc/HOL/Analysis/Derivative.thy (diff)
The file was modifiedsrc/HOL/Analysis/Elementary_Normed_Spaces.thy (diff)
The file was modifiedsrc/HOL/Deriv.thy (diff)
The file was modifiedsrc/HOL/Library/Extended_Nonnegative_Real.thy (diff)
Changeset 70530:80a1aa30e24d by haftmann:
avoid pseudo-collection to be used in generated proofs
The file was modifiedsrc/HOL/Rat.thy (diff)
Changeset 70529:050104f01bf9 by haftmann:
moved comment to approproiate place
The file was modifiedsrc/HOL/Fields.thy (diff)
The file was modifiedsrc/HOL/Rat.thy (diff)
Changeset 70528:e54caaa38ad9 by haftmann:
removed outcommented example which seems not to work as advertized
The file was modifiedsrc/HOL/Fields.thy (diff)
Changeset 70527: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 modifiedNEWS (diff)
The file was modifiedsrc/HOL/Library/Library.thy (diff)
The file was modifiedsrc/HOL/Word/Misc_Arithmetic.thy (diff)
The file was modifiedsrc/HOL/Word/Word.thy (diff)
The file was removedsrc/HOL/Library/Bit.thy
The file was removedsrc/HOL/Word/Bits_Bit.thy
Changeset 70526:972c0c744e7c by haftmann:
generalized type classes for parity to cover word types also, which contain zero divisors
The file was modifiedsrc/HOL/Groebner_Basis.thy (diff)
The file was modifiedsrc/HOL/Parity.thy (diff)
The file was modifiedsrc/HOL/Presburger.thy (diff)
Changeset 70525:7383930fc946 by haftmann:
slightly more specialized name for type class
The file was modifiedsrc/HOL/Code_Numeral.thy (diff)
The file was modifiedsrc/HOL/Divides.thy (diff)
The file was modifiedsrc/HOL/Groebner_Basis.thy (diff)
The file was modifiedsrc/HOL/Parity.thy (diff)
The file was modifiedsrc/HOL/Presburger.thy (diff)
The file was modifiedsrc/HOL/Real_Asymp/Multiseries_Expansion.thy (diff)
The file was modifiedsrc/HOL/Set_Interval.thy (diff)
The file was modifiedsrc/HOL/String.thy (diff)
The file was modifiedsrc/HOL/ex/Bit_Lists.thy (diff)
Changeset 70524:e939ea997f5f by haftmann:
dropped weaker legacy alias
The file was modifiedsrc/HOL/Parity.thy (diff)
The file was modifiedsrc/HOL/ex/Bit_Lists.thy (diff)
Changeset 70523:c832d431636b by haftmann:
slightly more stringent ordering of theorems
The file was modifiedsrc/HOL/Parity.thy (diff)
Changeset 70522:48609a6af1a0 by haftmann:
removed relics of ASCII syntax for indexed big operators
The file was modifiedNEWS (diff)
The file was modifiedsrc/HOL/Analysis/Abstract_Limits.thy (diff)
The file was modifiedsrc/HOL/Complete_Lattices.thy (diff)
The file was modifiedsrc/HOL/Computational_Algebra/Formal_Laurent_Series.thy (diff)
Changeset 70521:559f45528804 by haftmann:
dropped former legacy input abbreviations
The file was modifiedsrc/HOL/Main.thy (diff)
Changeset 70520:9bd8c16b6627 by haftmann:
using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax
The file was modifiedsrc/HOL/Library/Perm.thy (diff)
Changeset 70519:bba46912379e by haftmann:
prefer fixed simpset for proof procedure
The file was modifiedsrc/HOL/Library/Sum_of_Squares/sum_of_squares.ML (diff)
Changeset 70518:0f7edf0853df by haftmann:
tuned file system structure
The file was addedsrc/HOL/Library/Sum_of_Squares/positivstellensatz.ML
The file was modifiedsrc/HOL/Library/Sum_of_Squares.thy (diff)
The file was removedsrc/HOL/Library/positivstellensatz.ML
Changeset 70517:315489d836d8 by haftmann:
avoid spammed sledgehammer proofs
The file was modifiedsrc/HOL/Semiring_Normalization.thy (diff)