Skip to content
Success

Changes

Summary

  1. disable share_common_data for now (amending 0f8742b5a9e8) -- potentially more robust;
  2. merged
  3. load theories in stages, to reduce ML heap requirements;
  4. more complete graph;
  5. tuned messages;
  6. tuned signature;
  7. clarified signature;
  8. tuned important special case;
  9. tuned signature;
  10. more dump_checkpoints;
  11. clarified signature;
  12. clarified state variable: avoid extra mutability via Promise;
  13. Removal of the redundant ancestor Continuous_Extension
  14. Half of Brouwer_Fixpoint split off to form a separate theory: Retracts.
  15. Theory Derivative no longer depends on Path_Connected
Changeset 70655:f51955effb02 by wenzelm:
disable share_common_data for now (amending 0f8742b5a9e8) -- potentially more robust;
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 70654:cce7a95f6e0f by wenzelm:
merged
Changeset 70653:f7c5b30fc432 by wenzelm:
load theories in stages, to reduce ML heap requirements;
The file was modified src/Pure/PIDE/document_status.scala (diff)
The file was modified src/Pure/PIDE/headless.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 70652:d5e4231caa06 by wenzelm:
more complete graph;
The file was modified src/Pure/PIDE/resources.scala (diff)
Changeset 70651:d1d4a1b1ff1f by wenzelm:
tuned messages;
The file was modified src/Pure/General/graph.scala (diff)
Changeset 70650:fa04b549f652 by wenzelm:
tuned signature;
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 70649:9a40720750dc by wenzelm:
clarified signature;
The file was modified src/Pure/PIDE/headless.scala (diff)
Changeset 70648:60cb2bfea2d2 by wenzelm:
tuned important special case;
The file was modified src/Pure/PIDE/headless.scala (diff)
Changeset 70647:3047b7671279 by wenzelm:
tuned signature;
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/PIDE/headless.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 70646:a4d265a6c5cc by wenzelm:
more dump_checkpoints;
The file was modified src/HOL/ROOT (diff)
Changeset 70645:fc27cecb66d8 by wenzelm:
clarified signature;
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 70644:b23a6dfcfd57 by wenzelm:
clarified state variable: avoid extra mutability via Promise;
The file was modified src/Pure/PIDE/headless.scala (diff)
Changeset 70643:93a7a85de312 by paulson _lp15@cam.ac.uk_:
Removal of the redundant ancestor Continuous_Extension
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Retracts.thy (diff)
Changeset 70642:de9c4ed2d5df by paulson _lp15@cam.ac.uk_:
Half of Brouwer_Fixpoint split off to form a separate theory: Retracts.
The file was addedsrc/HOL/Analysis/Retracts.thy
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
Changeset 70641:0e2a065d6f31 by paulson _lp15@cam.ac.uk_:
Theory Derivative no longer depends on Path_Connected
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/Ordered_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Polytope.thy (diff)