Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. keep original bottom-up order of proof forks, which potentially reduces thread congestion due to Proofterm.consolidate;
  3. consolidate proofs more simultaneously;
  4. more informative task_statistics;
  5. more informative task_statistics;
  6. Merge
  7. New theorems and much tidying up of the old ones
  8. added 'solvers' option to Nunchaku
  9. Contravariant map on filters
Changeset 66170:cad55bc7e37d by wenzelm:
merged
Changeset 66169:8cfa8c7ee1f6 by wenzelm:
keep original bottom-up order of proof forks, which potentially reduces thread congestion due to Proofterm.consolidate;
The file was modified src/Pure/Isar/toplevel.ML (diff)
Changeset 66168:fcd09fc36d7f by wenzelm:
consolidate proofs more simultaneously;
The file was modified src/HOL/SPARK/Tools/spark_vcs.ML (diff)
The file was modified src/Pure/Concurrent/lazy.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 66167:1bd268ab885c by wenzelm:
more informative task_statistics;
The file was modified src/Pure/Concurrent/cache.ML (diff)
The file was modified src/Pure/Concurrent/lazy.ML (diff)
The file was modified src/Pure/Isar/code.ML (diff)
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/PIDE/document.ML (diff)
The file was modified src/Pure/Syntax/syntax.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 66166:c88d1c36c9c3 by wenzelm:
more informative task_statistics;
The file was modified src/Pure/Concurrent/event_timer.ML (diff)
The file was modified src/Pure/Concurrent/future.ML (diff)
The file was modified src/Pure/Concurrent/lazy.ML (diff)
The file was modified src/Pure/Concurrent/task_queue.ML (diff)
The file was modified src/Pure/PIDE/active.ML (diff)
The file was modified src/Pure/System/invoke_scala.ML (diff)
Changeset 66165:48cfbccaf3f4 by paulson _lp15@cam.ac.uk_:
Merge
Changeset 66164:2d79288b042c by paulson _lp15@cam.ac.uk_:
New theorems and much tidying up of the old ones
The file was modified src/HOL/Analysis/Borel_Space.thy (diff)
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Interval_Integral.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Set_Integral.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 66163:45d3d43abee7 by blanchet:
added 'solvers' option to Nunchaku
The file was modified src/HOL/Nunchaku/Nunchaku.thy (diff)
The file was modified src/HOL/Nunchaku/Tools/nunchaku.ML (diff)
The file was modified src/HOL/Nunchaku/Tools/nunchaku_commands.ML (diff)
The file was modified src/HOL/Nunchaku/Tools/nunchaku_tool.ML (diff)
Changeset 66162:65cd285f6b9c by eberlm _eberlm@in.tum.de_:
Contravariant map on filters
The file was modified src/HOL/Filter.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)