Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

  1. repaired proofs
  2. moved some theorems into HOL main corpus
  3. official fact collection sign_simps
  4. dropped unused session references
  5. clear separation of types for bits (False / True) and Z2 (0 / 1)
  6. dropped weaker legacy alias; modernized syntax
  7. dropped former legacy input abbreviations
Changeset 10463:c293c479d6b6 by haftmann:
repaired proofs
The file was modified thys/KD_Tree/Balanced.thy
Changeset 10462:a9d827f1c5b1 by haftmann:
moved some theorems into HOL main corpus
The file was modified thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy
The file was modified thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy
The file was modified thys/Gromov_Hyperbolicity/Morse_Gromov_Theorem.thy
The file was modified thys/KD_Tree/KDTree.thy
The file was modified thys/Sqrt_Babylonian/Sqrt_Babylonian_Auxiliary.thy
Changeset 10461:65974f61a998 by haftmann:
official fact collection sign_simps
The file was modified thys/Affine_Arithmetic/Counterclockwise_2D_Arbitrary.thy
The file was modified thys/Affine_Arithmetic/Executable_Euclidean_Space.thy
The file was modified thys/Count_Complex_Roots/Extended_Sturm.thy
The file was modified thys/DiscretePricing/CRR_Model.thy
The file was modified thys/Ergodic_Theory/Fekete.thy
The file was modified thys/Ergodic_Theory/Gouezel_Karlsson.thy
The file was modified thys/Ergodic_Theory/Invariants.thy
The file was modified thys/Gromov_Hyperbolicity/Isometries.thy
The file was modified thys/Gromov_Hyperbolicity/Isometries_Classification.thy
The file was modified thys/Gromov_Hyperbolicity/Metric_Completion.thy
The file was modified thys/IEEE_Floating_Point/IEEE_Properties.thy
The file was modified thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy
The file was modified thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Instantiation.thy
The file was modified thys/LinearQuantifierElim/Thys/FRE.thy
The file was modified thys/Multi_Party_Computation/Secure_Multiplication.thy
The file was modified thys/Neumann_Morgenstern_Utility/PMF_Composition.thy
The file was modified thys/Ordinary_Differential_Equations/IVP/Cones.thy
The file was modified thys/Planarity_Certificates/Planarity/Digraph_Map_Impl.thy
The file was modified thys/Polynomial_Interpolation/Missing_Polynomial.thy
The file was modified thys/Polynomial_Interpolation/Missing_Unsorted.thy
The file was modified thys/Source_Coding_Theorem/Source_Coding_Theorem.thy
The file was modified thys/Taylor_Models/Interval.thy
The file was modified thys/Taylor_Models/Interval_Approximation.thy
The file was modified thys/Winding_Number_Eval/Missing_Topology.thy
The file was modified thys/Winding_Number_Eval/Winding_Number_Eval_Examples.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
The file was modified thys/pGCL/Algebra.thy
The file was modified thys/pGCL/Continuity.thy
The file was modified thys/pGCL/Healthiness.thy
The file was modified thys/pGCL/Sublinearity.thy
The file was modified thys/pGCL/WellDefined.thy
Changeset 10460:415b7b57be74 by haftmann:
dropped unused session references
The file was modified thys/Deriving/ROOT
Changeset 10459:0546343b94d3 by haftmann:
clear separation of types for bits (False / True) and Z2 (0 / 1)
The file was addedthys/Gauss_Jordan/Code_Z2.thy
The file was modified thys/Gauss_Jordan/Examples_Gauss_Jordan_Abstract.thy
The file was modified thys/Gauss_Jordan/Examples_Gauss_Jordan_IArrays.thy
The file was removedthys/Gauss_Jordan/Code_Bit.thy
Changeset 10458:ee7d766eb01a by haftmann:
dropped weaker legacy alias;<br>modernized syntax
The file was modified thys/Constructive_Cryptography/More_CryptHOL.thy
The file was modified thys/Euler_Partition/Euler_Partition.thy
The file was modified thys/UTP/utp/utp_pred.thy
Changeset 10457:f6b91be1ab2d by haftmann:
dropped former legacy input abbreviations
The file was modified thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy
The file was modified thys/Graph_Saturation/CombinedCorrectness.thy
The file was modified thys/Graph_Saturation/GraphRewriting.thy
The file was modified thys/HOL-CSP/Process.thy
The file was modified thys/KD_Tree/Balanced.thy
The file was modified thys/Kruskal/UGraph_Impl.thy
The file was modified thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Construction.thy
The file was modified thys/Polynomials/MPoly_PM.thy
The file was modified thys/Transition_Systems_and_Automata/Automata/DBA/DBA_Combine.thy
The file was modified thys/Transition_Systems_and_Automata/Automata/DCA/DCA_Combine.thy
The file was modified thys/Transition_Systems_and_Automata/Automata/DRA/DRA_Combine.thy
The file was modified thys/UTP/toolkit/Countable_Set_Extra.thy
The file was modified thys/UTP/utp/utp_healthy.thy
The file was modified thys/UTP/utp/utp_rel_laws.thy

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

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