
 src/HOL/Library/Z2.thy (diff) 

 src/HOL/Data_Structures/AVL_Set.thy (diff) 
 src/HOL/Decision_Procs/Approximation_Bounds.thy (diff) 
 src/HOL/Library/Log_Nat.thy (diff) 
 src/HOL/Library/Tree_Real.thy (diff) 
 src/HOL/Rat.thy (diff) 
 src/HOL/Transcendental.thy (diff) 

 src/HOL/Library/Log_Nat.thy (diff) 

 src/HOL/Library/Type_Length.thy (diff) 
 src/HOL/ex/Word_Type.thy (diff) 

 NEWS (diff) 
 src/HOL/Analysis/Conformal_Mappings.thy (diff) 
 src/HOL/Decision_Procs/Approximation_Bounds.thy (diff) 
 src/HOL/Groups.thy (diff) 
 src/HOL/Library/Float.thy (diff) 
 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy (diff) 
 src/HOL/Rat.thy (diff) 
 src/HOL/Rings.thy (diff) 
 src/HOL/ex/Ballot.thy (diff) 

 src/HOL/Analysis/Conformal_Mappings.thy (diff) 
 src/HOL/Analysis/Derivative.thy (diff) 
 src/HOL/Analysis/Elementary_Normed_Spaces.thy (diff) 
 src/HOL/Deriv.thy (diff) 
 src/HOL/Library/Extended_Nonnegative_Real.thy (diff) 

 src/HOL/Rat.thy (diff) 

 src/HOL/Fields.thy (diff) 
 src/HOL/Rat.thy (diff) 

 src/HOL/Fields.thy (diff) 

 src/HOL/Library/Z2.thy 
 src/HOL/Word/Bits_Z2.thy 
 NEWS (diff) 
 src/HOL/Library/Library.thy (diff) 
 src/HOL/Word/Misc_Arithmetic.thy (diff) 
 src/HOL/Word/Word.thy (diff) 
 src/HOL/Library/Bit.thy 
 src/HOL/Word/Bits_Bit.thy 
Changeset
70526:972c0c744e7c
by haftmann:
generalized type classes for parity to cover word types also, which contain zero divisors

 src/HOL/Groebner_Basis.thy (diff) 
 src/HOL/Parity.thy (diff) 
 src/HOL/Presburger.thy (diff) 

 src/HOL/Code_Numeral.thy (diff) 
 src/HOL/Divides.thy (diff) 
 src/HOL/Groebner_Basis.thy (diff) 
 src/HOL/Parity.thy (diff) 
 src/HOL/Presburger.thy (diff) 
 src/HOL/Real_Asymp/Multiseries_Expansion.thy (diff) 
 src/HOL/Set_Interval.thy (diff) 
 src/HOL/String.thy (diff) 
 src/HOL/ex/Bit_Lists.thy (diff) 

 src/HOL/Parity.thy (diff) 
 src/HOL/ex/Bit_Lists.thy (diff) 

 src/HOL/Parity.thy (diff) 

 NEWS (diff) 
 src/HOL/Analysis/Abstract_Limits.thy (diff) 
 src/HOL/Complete_Lattices.thy (diff) 
 src/HOL/Computational_Algebra/Formal_Laurent_Series.thy (diff) 

 src/HOL/Main.thy (diff) 

 src/HOL/Library/Perm.thy (diff) 

 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML (diff) 

 src/HOL/Library/Sum_of_Squares/positivstellensatz.ML 
 src/HOL/Library/Sum_of_Squares.thy (diff) 
 src/HOL/Library/positivstellensatz.ML 

 src/HOL/Semiring_Normalization.thy (diff) 