Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. eliminated irregular aliasses
  2. avoid references to lemmas designed for prover tools
  3. clarified theorem names
  4. eliminated irregular aliasses
  5. more standardized theorem names for facts involving the div and mod identity
  6. transfer rules for divides relation on integer and natural
  7. more standardized names
  8. added lemma
  9. de-orphanized declaration
Changeset 64246:15d1ee6e847b by haftmann:
eliminated irregular aliasses
The file was modified NEWS (diff)
The file was modified src/HOL/Algebra/IntRing.thy (diff)
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/Decision_Procs/Approximation.thy (diff)
The file was modified src/HOL/Decision_Procs/Cooper.thy (diff)
The file was modified src/HOL/Decision_Procs/MIR.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/Hoare/Arith2.thy (diff)
The file was modified src/HOL/Library/Float.thy (diff)
The file was modified src/HOL/Library/RBT_Impl.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Int2.thy (diff)
The file was modified src/HOL/Old_Number_Theory/IntPrimes.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy (diff)
The file was modified src/HOL/Presburger.thy (diff)
The file was modified src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy (diff)
The file was modified src/HOL/SPARK/Manual/Example_Verification.thy (diff)
The file was modified src/HOL/Word/Bit_Representation.thy (diff)
The file was modified src/HOL/Word/Word_Miscellaneous.thy (diff)
Changeset 64245:3d00821444fc by haftmann:
avoid references to lemmas designed for prover tools
The file was modified src/HOL/Word/Word_Miscellaneous.thy (diff)
Changeset 64244:e7102c40783c by haftmann:
clarified theorem names
The file was modified NEWS (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/Presburger.thy (diff)
The file was modified src/HOL/Tools/Qelim/cooper.ML (diff)
The file was modified src/HOL/Tools/nat_numeral_simprocs.ML (diff)
Changeset 64243:aee949f6642d by haftmann:
eliminated irregular aliasses
The file was modified NEWS (diff)
The file was modified src/HOL/Decision_Procs/Approximation.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/Library/RBT_Impl.thy (diff)
The file was modified src/HOL/Number_Theory/Eratosthenes.thy (diff)
The file was modified src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Pocklington.thy (diff)
The file was modified src/HOL/Tools/Qelim/cooper.ML (diff)
The file was modified src/HOL/Word/Word.thy (diff)
Changeset 64242:93c6f0da5c70 by haftmann:
more standardized theorem names for facts involving the div and mod identity
The file was modified NEWS (diff)
The file was modified src/Doc/Tutorial/Rules/Force.thy (diff)
The file was modified src/Doc/Tutorial/Rules/Forward.thy (diff)
The file was modified src/Doc/Tutorial/Types/Numbers.thy (diff)
The file was modified src/Doc/Tutorial/document/numerics.tex (diff)
The file was modified src/Doc/Tutorial/document/rules.tex (diff)
The file was modified src/HOL/Data_Structures/RBT_Set.thy (diff)
The file was modified src/HOL/Decision_Procs/Approximation.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/GCD.thy (diff)
The file was modified src/HOL/Hoare_Parallel/OG_Examples.thy (diff)
The file was modified src/HOL/Library/Code_Target_Int.thy (diff)
The file was modified src/HOL/Library/Code_Target_Nat.thy (diff)
The file was modified src/HOL/Library/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Library/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Library/Stream.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/StarDef.thy (diff)
The file was modified src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff)
The file was modified src/HOL/Number_Theory/Pocklington.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Pocklington.thy (diff)
The file was modified src/HOL/Presburger.thy (diff)
The file was modified src/HOL/Rings.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/Word.thy (diff)
The file was modified src/HOL/ex/Transfer_Ex.thy (diff)
The file was modified src/HOL/ex/Word_Type.thy (diff)
Changeset 64241:430d74089d4d by haftmann:
transfer rules for divides relation on integer and natural
The file was modified src/HOL/Code_Numeral.thy (diff)
Changeset 64240:eabf80376aab by haftmann:
more standardized names
The file was modified NEWS (diff)
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/Polytope.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/Decision_Procs/Approximation.thy (diff)
The file was modified src/HOL/Decision_Procs/Ferrack.thy (diff)
The file was modified src/HOL/Decision_Procs/MIR.thy (diff)
The file was modified src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy (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/GCD.thy (diff)
The file was modified src/HOL/Library/Float.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_FPS.thy (diff)
The file was modified src/HOL/Library/Polynomial_Factorial.thy (diff)
The file was modified src/HOL/Library/Stirling.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HDeriv.thy (diff)
The file was modified src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff)
The file was modified src/HOL/Number_Theory/Gauss.thy (diff)
The file was modified src/HOL/Old_Number_Theory/EvenOdd.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Gauss.thy (diff)
The file was modified src/HOL/Old_Number_Theory/IntPrimes.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy (diff)
The file was modified src/HOL/Probability/SPMF.thy (diff)
The file was modified src/HOL/Quotient_Examples/Quotient_Rat.thy (diff)
The file was modified src/HOL/Rat.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
The file was modified src/HOL/Tools/numeral_simprocs.ML (diff)
The file was modified src/HOL/ex/Simproc_Tests.thy (diff)
Changeset 64239:de5cd9217d4c by haftmann:
added lemma
The file was modified src/HOL/Rings.thy (diff)
Changeset 64238:b60a9752b6d0 by haftmann:
de-orphanized declaration
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/Num.thy (diff)