Skip to content
Failed

Changes

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

Summary

  1. dummy Admin/components/go to avoid crash of Jenkins (see 38bbc2ff3c24);
Changeset 80043:a0210a24b547 by wenzelm:
dummy Admin/components/go to avoid crash of Jenkins (see 38bbc2ff3c24);
The file was addedAdmin/components/go

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. tuned proofs: avoid z3 to make it work on arm64-linux;
  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;
Changeset 14164:1a2512112874 by wenzelm:
tuned proofs: avoid z3 to make it work on arm64-linux;
The file was modified thys/Budan_Fourier/BF_Misc.thy
The file was modified thys/Three_Squares/Quadratic_Forms.thy
The file was modified thys/Three_Squares/Three_Squares.thy
Changeset 14163: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
The file was modified thys/Core_SC_DOM/common/monads/NodeMonad.thy
The file was modified thys/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy
Changeset 14162:d9d45697c125 by wenzelm:
tuned proofs: avoid z3 to make it work on arm64-linux;
The file was modified thys/Universal_Turing_Machine/BlanksDoNotMatter.thy
The file was modified thys/Universal_Turing_Machine/HaltingProblems_K_H.thy
The file was modified thys/Universal_Turing_Machine/Numerals.thy
The file was modified thys/Universal_Turing_Machine/Recursive.thy
The file was modified thys/Universal_Turing_Machine/StrongCopyTM.thy
The file was modified thys/Universal_Turing_Machine/TM_Playground.thy
The file was modified thys/Universal_Turing_Machine/TuringComputable.thy
The file was modified thys/Universal_Turing_Machine/TuringComputable_aux.thy
The file was modified thys/Universal_Turing_Machine/Turing_HaltingConditions.thy
The file was modified thys/Universal_Turing_Machine/UTM.thy
The file was modified thys/Universal_Turing_Machine/WeakCopyTM.thy
Changeset 14161:455b44957816 by wenzelm:
tuned proofs: avoid z3 to make it work on arm64-linux;
The file was modified thys/Word_Lib/More_Word.thy
The file was modified thys/Word_Lib/More_Word_Operations.thy
The file was modified thys/Word_Lib/Reversed_Bit_Lists.thy
The file was modified thys/Word_Lib/Signed_Division_Word.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
Changeset 14160:d0bd37a0fea4 by wenzelm:
tuned proofs: avoid z3 to make it work on arm64-linux;
The file was modified thys/Padic_Ints/Cring_Poly.thy
The file was modified thys/Padic_Ints/Extended_Int.thy
The file was modified thys/Padic_Ints/Function_Ring.thy
The file was modified thys/Padic_Ints/Hensels_Lemma.thy
The file was modified thys/Padic_Ints/Padic_Int_Polynomials.thy
The file was modified thys/Padic_Ints/Padic_Int_Topology.thy
The file was modified thys/Padic_Ints/Padic_Integers.thy
The file was modified thys/Padic_Ints/Zp_Compact.thy