Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. tuned;
  3. clarified file names;
  4. SML/NJ is no longer supported;
  5. dropped various legacy fact bindings and tuned proofs
  6. separated potentially conflicting type class instance into separate theory
  7. gcd instances for poly
  8. more sophisticated GCD syntax
  9. cleansed junk-producing interpretations for gcd/lcm on nat altogether
  10. dropped various legacy fact bindings
  11. generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
  12. more theorems concerning gcd/lcm/Gcd/Lcm
  13. further generalization and polishing
  14. pulled out legacy aliasses and infamous dvd interpretations into theory appendix
  15. prefer abbreviations for compound operators INFIMUM and SUPREMUM
  16. consolidated name
Changeset 62357:ab76bd43c14a by wenzelm:
merged
Changeset 62356:e307a410f46c by wenzelm:
tuned;
The file was modified src/Pure/General/secure.ML (diff)
The file was modified src/Pure/ML/install_pp_polyml.ML (diff)
The file was modified src/Pure/RAW/ROOT_polyml.ML (diff)
The file was modified src/Pure/ROOT.ML (diff)
Changeset 62355:00f7618a9f2b by wenzelm:
clarified file names;
The file was addedsrc/Pure/ML/exn_output.ML
The file was addedsrc/Pure/ML/exn_properties.ML
The file was addedsrc/Pure/ML/ml_compiler.ML
The file was modified src/Pure/ROOT (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was removedsrc/Pure/ML/exn_output_polyml.ML
The file was removedsrc/Pure/ML/exn_properties_polyml.ML
The file was removedsrc/Pure/ML/ml_compiler_polyml.ML
Changeset 62354:fdd6989cc8a0 by wenzelm:
SML/NJ is no longer supported;
The file was modified Admin/Release/CHECKLIST (diff)
The file was modified Admin/isatest/isatest-makeall (diff)
The file was modified Admin/isatest/isatest-makedist (diff)
The file was modified Admin/isatest/isatest-stats (diff)
The file was modified NEWS (diff)
The file was modified etc/settings (diff)
The file was modified lib/scripts/getsettings (diff)
The file was modified src/Doc/Implementation/ML.thy (diff)
The file was modified src/Doc/ROOT (diff)
The file was modified src/Doc/System/Basics.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML (diff)
The file was modified src/Pure/General/socket_io.ML (diff)
The file was modified src/Pure/ML/exn_output_polyml.ML (diff)
The file was modified src/Pure/ML/ml_compiler_polyml.ML (diff)
The file was modified src/Pure/ML/ml_env.ML (diff)
The file was modified src/Pure/ML/ml_parse.ML (diff)
The file was modified src/Pure/RAW/ROOT_polyml.ML (diff)
The file was modified src/Pure/RAW/compiler_polyml.ML (diff)
The file was modified src/Pure/RAW/ml_system.ML (diff)
The file was modified src/Pure/RAW/use_context.ML (diff)
The file was modified src/Pure/ROOT (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)
The file was modified src/Tools/ROOT (diff)
The file was modified src/Tools/Spec_Check/spec_check.ML (diff)
The file was removedAdmin/isatest/settings/at-sml-dev-e
The file was removedlib/scripts/run-smlnj
The file was removedsrc/Pure/ML/exn_output.ML
The file was removedsrc/Pure/ML/exn_properties_dummy.ML
The file was removedsrc/Pure/ML/ml_compiler.ML
The file was removedsrc/Pure/RAW/ROOT_smlnj.ML
The file was removedsrc/Pure/RAW/ml_name_space.ML
The file was removedsrc/Pure/RAW/overloading_smlnj.ML
The file was removedsrc/Pure/RAW/pp_dummy.ML
The file was removedsrc/Pure/RAW/proper_int.ML
The file was removedsrc/Pure/RAW/single_assignment.ML
The file was removedsrc/Pure/RAW/thread_dummy.ML
The file was removedsrc/Pure/RAW/universal.ML
Changeset 62353:7f927120b5a2 by haftmann:
dropped various legacy fact bindings and tuned proofs
The file was modified NEWS (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/Number_Theory/Cong.thy (diff)
The file was modified src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff)
Changeset 62352:35a9e1cbb5b3 by haftmann:
separated potentially conflicting type class instance into separate theory
The file was addedsrc/HOL/Library/Polynomial_GCD_euclidean.thy
The file was modified NEWS (diff)
The file was modified src/HOL/Codegenerator_Test/Candidates.thy (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Library/Polynomial.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/Library/Poly_Deriv.thy
Changeset 62351:fd049b54ad68 by haftmann:
gcd instances for poly
The file was modified src/HOL/Library/Polynomial.thy (diff)
Changeset 62350:66a381d3f88f by haftmann:
more sophisticated GCD syntax
The file was modified src/HOL/GCD.thy (diff)
Changeset 62349:7c23469b5118 by haftmann:
cleansed junk-producing interpretations for gcd/lcm on nat altogether
The file was modified src/HOL/Algebra/Exponent.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/NSA/Examples/NSPrimes.thy (diff)
The file was modified src/HOL/Number_Theory/Cong.thy (diff)
The file was modified src/HOL/Number_Theory/Eratosthenes.thy (diff)
The file was modified src/HOL/Number_Theory/Pocklington.thy (diff)
The file was modified src/HOL/Number_Theory/Primes.thy (diff)
The file was modified src/HOL/Number_Theory/UniqueFactorization.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Primes.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
Changeset 62348:9a5f43dac883 by haftmann:
dropped various legacy fact bindings
The file was modified NEWS (diff)
The file was modified src/HOL/Algebra/Exponent.thy (diff)
The file was modified src/HOL/Algebra/IntRing.thy (diff)
The file was modified src/HOL/Archimedean_Field.thy (diff)
The file was modified src/HOL/Decision_Procs/Rat_Pair.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/GCD.thy (diff)
The file was modified src/HOL/Groups.thy (diff)
The file was modified src/HOL/Inequalities.thy (diff)
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/Isar_Examples/Fibonacci.thy (diff)
The file was modified src/HOL/Library/Float.thy (diff)
The file was modified src/HOL/Library/Numeral_Type.thy (diff)
The file was modified src/HOL/Library/Old_SMT/old_smt_normalize.ML (diff)
The file was modified src/HOL/Matrix_LP/ComputeFloat.thy (diff)
The file was modified src/HOL/Matrix_LP/ComputeNumeral.thy (diff)
The file was modified src/HOL/Nat_Transfer.thy (diff)
The file was modified src/HOL/Num.thy (diff)
The file was modified src/HOL/Number_Theory/Cong.thy (diff)
The file was modified src/HOL/Number_Theory/Euclidean_Algorithm.thy (diff)
The file was modified src/HOL/Number_Theory/Factorial_Ring.thy (diff)
The file was modified src/HOL/Number_Theory/Fib.thy (diff)
The file was modified src/HOL/Number_Theory/Gauss.thy (diff)
The file was modified src/HOL/Number_Theory/Pocklington.thy (diff)
The file was modified src/HOL/Number_Theory/Primes.thy (diff)
The file was modified src/HOL/Number_Theory/Residues.thy (diff)
The file was modified src/HOL/Number_Theory/UniqueFactorization.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Legacy_GCD.thy (diff)
The file was modified src/HOL/Old_Number_Theory/Primes.thy (diff)
The file was modified src/HOL/Presburger.thy (diff)
The file was modified src/HOL/Rat.thy (diff)
The file was modified src/HOL/Real.thy (diff)
The file was modified src/HOL/Tools/Qelim/cooper.ML (diff)
The file was modified src/HOL/Word/Word.thy (diff)
The file was modified src/HOL/ex/LocaleTest2.thy (diff)
The file was modified src/HOL/ex/NatSum.thy (diff)
The file was modified src/HOL/ex/Sqrt.thy (diff)
The file was modified src/HOL/ex/Transfer_Int_Nat.thy (diff)
Changeset 62347:2230b7047376 by haftmann:
generalized some lemmas;<br>moved some lemmas in more appropriate places;<br>deleted potentially dangerous simp rule
The file was modified NEWS (diff)
The file was modified src/HOL/Algebra/Coset.thy (diff)
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/Fields.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/Groups.thy (diff)
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/NthRoot.thy (diff)
The file was modified src/HOL/Power.thy (diff)
The file was modified src/HOL/Real.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/Transcendental.thy (diff)
Changeset 62346:97f2ed240431 by haftmann:
more theorems concerning gcd/lcm/Gcd/Lcm
The file was modified src/HOL/GCD.thy (diff)
Changeset 62345:e66d7841d5a2 by haftmann:
further generalization and polishing
The file was modified NEWS (diff)
The file was modified src/HOL/GCD.thy (diff)
Changeset 62344:759d684c0e60 by haftmann:
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
Changeset 62343:24106dc44def by haftmann:
prefer abbreviations for compound operators INFIMUM and SUPREMUM
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/HOL/Algebra/AbelCoset.thy (diff)
The file was modified src/HOL/Algebra/Coset.thy (diff)
The file was modified src/HOL/Auth/Guard/Proto.thy (diff)
The file was modified src/HOL/Auth/Message.thy (diff)
The file was modified src/HOL/Auth/Recur.thy (diff)
The file was modified src/HOL/Auth/Smartcard/ShoupRubin.thy (diff)
The file was modified src/HOL/Auth/Smartcard/ShoupRubinBella.thy (diff)
The file was modified src/HOL/Auth/Smartcard/Smartcard.thy (diff)
The file was modified src/HOL/BNF_Cardinal_Order_Relation.thy (diff)
The file was modified src/HOL/Cardinals/Wellorder_Relation.thy (diff)
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Conditionally_Complete_Lattices.thy (diff)
The file was modified src/HOL/Enum.thy (diff)
The file was modified src/HOL/Filter.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Hoare_Parallel/OG_Hoare.thy (diff)
The file was modified src/HOL/Hoare_Parallel/RG_Hoare.thy (diff)
The file was modified src/HOL/IMP/Denotational.thy (diff)
The file was modified src/HOL/Library/Countable_Set_Type.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Library/FSet.thy (diff)
The file was modified src/HOL/Library/Finite_Lattice.thy (diff)
The file was modified src/HOL/Library/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Library/Liminf_Limsup.thy (diff)
The file was modified src/HOL/Library/Lub_Glb.thy (diff)
The file was modified src/HOL/Library/Option_ord.thy (diff)
The file was modified src/HOL/Library/Product_Order.thy (diff)
The file was modified src/HOL/Lifting_Set.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Integration.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Number_Theory/MiscAlgebra.thy (diff)
The file was modified src/HOL/Probability/Caratheodory.thy (diff)
The file was modified src/HOL/Probability/Complete_Measure.thy (diff)
The file was modified src/HOL/Probability/Embed_Measure.thy (diff)
The file was modified src/HOL/Probability/Fin_Map.thy (diff)
The file was modified src/HOL/Probability/Independent_Family.thy (diff)
The file was modified src/HOL/Probability/Infinite_Product_Measure.thy (diff)
The file was modified src/HOL/Probability/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Probability/Measurable.thy (diff)
The file was modified src/HOL/Probability/Measure_Space.thy (diff)
The file was modified src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy (diff)
The file was modified src/HOL/Probability/Probability_Measure.thy (diff)
The file was modified src/HOL/Probability/Radon_Nikodym.thy (diff)
The file was modified src/HOL/Probability/Regularity.thy (diff)
The file was modified src/HOL/Probability/Sigma_Algebra.thy (diff)
The file was modified src/HOL/Relation.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_comp_tactics.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_tactics.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_util.ML (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
The file was modified src/HOL/Transitive_Closure.thy (diff)
The file was modified src/HOL/UNITY/Comp/Alloc.thy (diff)
The file was modified src/HOL/UNITY/ELT.thy (diff)
The file was modified src/HOL/UNITY/Extend.thy (diff)
The file was modified src/HOL/UNITY/ProgressSets.thy (diff)
The file was modified src/HOL/UNITY/Rename.thy (diff)
The file was modified src/HOL/UNITY/SubstAx.thy (diff)
The file was modified src/HOL/UNITY/Transformers.thy (diff)
The file was modified src/HOL/UNITY/Union.thy (diff)
The file was modified src/HOL/UNITY/WFair.thy (diff)
Changeset 62342:1cf129590be8 by haftmann:
consolidated name
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/Tools/Nitpick/nitpick_hol.ML (diff)
The file was modified src/HOL/Tools/hologic.ML (diff)
The file was modified src/HOL/Tools/lin_arith.ML (diff)