Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
  3. avoid multiple PIDE markup due to (potentially infinite) backtracking;
  4. more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;
  5. more lemmas
  6. updated CVC4 component
  7. tuning
  8. more uniform treatment of codatatype vs. datatype map and rel theorem generation (towards nonuniform codatatypes)
  9. added lemma
Changeset 64422:efdd4c5daf7d by wenzelm:
merged
Changeset 64421:681fae6b00b5 by wenzelm:
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
The file was modified src/Pure/Isar/token.ML (diff)
Changeset 64420:2efc128370fa by wenzelm:
avoid multiple PIDE markup due to (potentially infinite) backtracking;
The file was modified src/Pure/Isar/proof.ML (diff)
Changeset 64419:0f3b0a929c02 by wenzelm:
more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;
The file was modified src/Pure/Admin/build_history.scala (diff)
Changeset 64418:91eae3a1be51 by fleury _mathias.fleury@mpi-inf.mpg.de_:
more lemmas
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Multiset_Order.thy (diff)
Changeset 64417:7f0edcc6c3d3 by blanchet:
updated CVC4 component
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
Changeset 64416:9312408aec32 by blanchet:
tuning
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
Changeset 64415:7ca48c274553 by blanchet:
more uniform treatment of codatatype vs. datatype map and rel theorem generation (towards nonuniform codatatypes)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML (diff)
Changeset 64414:f8be2208e99c by nipkow:
added lemma
The file was modified src/HOL/Library/Tree.thy (diff)