Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. proper Go setup, following Isabelle/1e7d4372fe3d;
  2. tuned proofs: avoid z3 to make it work on arm64-linux;
  3. tuned proofs: avoid z3 to make it work on arm64-linux;
  4. tuned proofs: avoid z3 to make it work on arm64-linux;
  5. tuned proofs: avoid z3 to make it work on arm64-linux;
  6. tuned proofs: avoid z3 to make it work on arm64-linux;
  7. updates to new time function generator that now translates undefined to undefined, not 0
  8. Fixes mostly for log_mono aliasing
  9. Brought this new entry up-to-date with the development version
Changeset 14878:8d8259071915 by wenzelm:
proper Go setup, following Isabelle/1e7d4372fe3d;
The file was modified thys/Go/code_go.ML (diff)
Changeset 14877:1a2512112874 by wenzelm:
tuned proofs: avoid z3 to make it work on arm64-linux;
The file was modified thys/Budan_Fourier/BF_Misc.thy (diff)
The file was modified thys/Three_Squares/Quadratic_Forms.thy (diff)
The file was modified thys/Three_Squares/Three_Squares.thy (diff)
Changeset 14876:d8244335636c by wenzelm:
tuned proofs: avoid z3 to make it work on arm64-linux;
The file was modified thys/Core_SC_DOM/common/monads/CharacterDataMonad.thy (diff)
The file was modified thys/Core_SC_DOM/common/monads/NodeMonad.thy (diff)
The file was modified thys/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy (diff)
Changeset 14875:d9d45697c125 by wenzelm:
tuned proofs: avoid z3 to make it work on arm64-linux;
The file was modified thys/Universal_Turing_Machine/BlanksDoNotMatter.thy (diff)
The file was modified thys/Universal_Turing_Machine/HaltingProblems_K_H.thy (diff)
The file was modified thys/Universal_Turing_Machine/Numerals.thy (diff)
The file was modified thys/Universal_Turing_Machine/Recursive.thy (diff)
The file was modified thys/Universal_Turing_Machine/StrongCopyTM.thy (diff)
The file was modified thys/Universal_Turing_Machine/TM_Playground.thy (diff)
The file was modified thys/Universal_Turing_Machine/TuringComputable.thy (diff)
The file was modified thys/Universal_Turing_Machine/TuringComputable_aux.thy (diff)
The file was modified thys/Universal_Turing_Machine/Turing_HaltingConditions.thy (diff)
The file was modified thys/Universal_Turing_Machine/UTM.thy (diff)
The file was modified thys/Universal_Turing_Machine/WeakCopyTM.thy (diff)
Changeset 14874:455b44957816 by wenzelm:
tuned proofs: avoid z3 to make it work on arm64-linux;
The file was modified thys/Word_Lib/More_Word.thy (diff)
The file was modified thys/Word_Lib/More_Word_Operations.thy (diff)
The file was modified thys/Word_Lib/Reversed_Bit_Lists.thy (diff)
The file was modified thys/Word_Lib/Signed_Division_Word.thy (diff)
The file was modified thys/Word_Lib/Word_Lemmas.thy (diff)
Changeset 14873:d0bd37a0fea4 by wenzelm:
tuned proofs: avoid z3 to make it work on arm64-linux;
The file was modified thys/Padic_Ints/Cring_Poly.thy (diff)
The file was modified thys/Padic_Ints/Extended_Int.thy (diff)
The file was modified thys/Padic_Ints/Function_Ring.thy (diff)
The file was modified thys/Padic_Ints/Hensels_Lemma.thy (diff)
The file was modified thys/Padic_Ints/Padic_Int_Polynomials.thy (diff)
The file was modified thys/Padic_Ints/Padic_Int_Topology.thy (diff)
The file was modified thys/Padic_Ints/Padic_Integers.thy (diff)
The file was modified thys/Padic_Ints/Zp_Compact.thy (diff)
Changeset 14872:bd6e0a8eeb23 by nipkow:
updates to new time function generator that now translates undefined to undefined, not 0
The file was modified thys/Amortized_Complexity/Splay_Tree_Analysis_Base.thy (diff)
Changeset 14871:18437ad04fb8 by paulson _lp15@cam.ac.uk_:
Fixes mostly for log_mono aliasing
The file was modified thys/Frequency_Moments/Frequency_Moment_0.thy (diff)
The file was modified thys/Frequency_Moments/Frequency_Moments_Preliminary_Results.thy (diff)
The file was modified thys/MDP-Algorithms/Splitting_Methods_Fin.thy (diff)
The file was modified thys/Markov_Models/ex/Crowds_Protocol.thy (diff)
The file was modified thys/Probabilistic_While/Fast_Dice_Roll.thy (diff)
The file was modified thys/Source_Coding_Theorem/Source_Coding_Theorem.thy (diff)
Changeset 14870:c6e769593bac by paulson _lp15@cam.ac.uk_:
Brought this new entry up-to-date with the development version
The file was modified thys/Continued_Fractions/Continued_Fractions.thy (diff)
The file was modified thys/Continued_Fractions/Sqrt_Nat_Cfrac.thy (diff)