Skip to content
[Jenkins]Jenkins
log in
Success

Changes

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

Summary

  1. compactified specification of type class parity
  2. generalized
  3. explicit annotation of lemma duplicates
  4. merged
  5. clarified proof_body: cover zboxes from zproof;
  6. pro-forma support for optional zproof: no proper content yet;
  7. clarified signature: follow Term.could_unify;
  8. clarified bootstrap --- modules related to proofterm.ML;
  9. clarified path time heuristic: configurable parameters for larger search space;
  10. clarified heuristics toString; add generator description to schedule;
  11. tuned;
  12. add heuristic for non-scheduled (standard) build behaviour;
  13. proper unused nodes;
  14. clarified schedule message;
  15. proper parallel paths;
  16. clarified build schedule host: more operations;
  17. clarified path heuristic;
  18. clarified graph operations in timing heuristic;
  19. merged
  20. added and removed [simp]s
Changeset 79118:486a32079c60 by haftmann:
compactified specification of type class parity
The file was modified NEWS
The file was modified src/HOL/Library/Word.thy
The file was modified src/HOL/Parity.thy
Changeset 79117:7476818dfd5d by haftmann:
generalized
The file was modified src/HOL/Bit_Operations.thy
The file was modified src/HOL/Parity.thy
Changeset 79116:b90bf6636260 by haftmann:
explicit annotation of lemma duplicates
The file was modified src/HOL/Bit_Operations.thy
Changeset 79115:0c7de2ae814b by wenzelm:
merged
Changeset 79114:686b7b14d041 by wenzelm:
clarified proof_body: cover zboxes from zproof;
The file was modified src/Pure/Proof/extraction.ML
The file was modified src/Pure/proofterm.ML
The file was modified src/Pure/thm.ML
The file was modified src/Pure/zterm.ML
Changeset 79113:5109e4b2a292 by wenzelm:
pro-forma support for optional zproof: no proper content yet;
The file was modified src/HOL/Tools/datatype_realizer.ML
The file was modified src/Pure/Isar/proof.ML
The file was modified src/Pure/Isar/toplevel.ML
The file was modified src/Pure/Proof/extraction.ML
The file was modified src/Pure/global_theory.ML
The file was modified src/Pure/goal.ML
The file was modified src/Pure/proofterm.ML
The file was modified src/Pure/thm.ML
The file was modified src/Pure/zterm.ML
Changeset 79112:fd9de06c0ecf by wenzelm:
clarified signature: follow Term.could_unify;
The file was modified src/Pure/proofterm.ML
Changeset 79111:8fb4013f2ac2 by wenzelm:
clarified bootstrap --- modules related to proofterm.ML;
The file was modified src/Pure/ROOT.ML
Changeset 79110:ff68cbfa3550 by fabian huch _huch@in.tum.de_:
clarified path time heuristic: configurable parameters for larger search space;
The file was modified src/Pure/Tools/build_schedule.scala
Changeset 79109:c1255d9870f6 by fabian huch _huch@in.tum.de_:
clarified heuristics toString;<br>add generator description to schedule;
The file was modified src/Pure/Tools/build_schedule.scala
Changeset 79108:ed00312f694f by fabian huch _huch@in.tum.de_:
tuned;
The file was modified src/Pure/Tools/build_schedule.scala
Changeset 79107:f5a2f956b531 by fabian huch _huch@in.tum.de_:
add heuristic for non-scheduled (standard) build behaviour;
The file was modified src/Pure/Tools/build_schedule.scala
Changeset 79106:91955d607aad by fabian huch _huch@in.tum.de_:
proper unused nodes;
The file was modified src/Pure/Tools/build_schedule.scala
Changeset 79105:6e92475ff925 by fabian huch _huch@in.tum.de_:
clarified schedule message;
The file was modified src/Pure/Tools/build_schedule.scala
Changeset 79104:e7ab5f4ed401 by fabian huch _huch@in.tum.de_:
proper parallel paths;
The file was modified src/Pure/Tools/build_schedule.scala
Changeset 79103:883f61f0beda by fabian huch _huch@in.tum.de_:
clarified build schedule host: more operations;
The file was modified src/Pure/Tools/build_schedule.scala
Changeset 79102:4d5f878665a3 by fabian huch _huch@in.tum.de_:
clarified path heuristic;
The file was modified src/Pure/Tools/build_schedule.scala
Changeset 79101:4e47b34fbb8e by fabian huch _huch@in.tum.de_:
clarified graph operations in timing heuristic;
The file was modified src/Pure/Tools/build_schedule.scala
Changeset 79100:e103e3cef3cb by nipkow:
merged
Changeset 79099:05a753360b25 by nipkow:
added and removed [simp]s
The file was modified src/HOL/Boolean_Algebras.thy
The file was modified src/HOL/Lattices.thy
The file was modified src/HOL/Set.thy

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

Summary

  1. adadpted to [simp] changes in distrib
Changeset 13910:ab6fb0658236 by nipkow:
adadpted to [simp] changes in distrib
The file was modified thys/Polynomials/Power_Products.thy
The file was modified thys/Progress_Tracking/Combined.thy
The file was modified thys/SenSocialChoice/Arrow.thy