Skip to content
Success

Changes

Summary

  1. explicit option metric_argo_timeout, with reasonable default for Raspberry Pi;
  2. tuned;
  3. repackage minisat-2.2.1 with cygwin1.dll: required to run the executable without existing Cygwin context (normally provided by bash_process);
  4. discontinued redundant document_preprocessor: in the worst case, a plain-old document/build script will do;
  5. clarified messages, depending on option "document_echo";
  6. just one cache, via HTML_Context, via Sessions.Store or Session;
  7. merged
  8. new lemmas about convex, concave functions, + tidying
Changeset 74736:df4449c6eff1 by wenzelm:
explicit option metric_argo_timeout, with reasonable default for Raspberry Pi;
The file was modified src/HOL/Analysis/ex/Metric_Arith_Examples.thy (diff)
The file was modified src/HOL/Analysis/metric_arith.ML (diff)
Changeset 74735:0580ae467ecb by wenzelm:
tuned;
The file was modified src/HOL/ex/Argo_Examples.thy (diff)
Changeset 74734:f345da8defff by wenzelm:
repackage minisat-2.2.1 with cygwin1.dll: required to run the executable without existing Cygwin context (normally provided by bash_process);
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified src/Pure/Admin/build_minisat.scala (diff)
Changeset 74733:255e651a4c5f by wenzelm:
discontinued redundant document_preprocessor: in the worst case, a plain-old document/build script will do;
The file was modified NEWS (diff)
The file was modified etc/options (diff)
The file was modified src/Doc/System/Sessions.thy (diff)
The file was modified src/Pure/Thy/document_build.scala (diff)
Changeset 74732:015282fb3e31 by wenzelm:
clarified messages, depending on option "document_echo";
The file was modified NEWS (diff)
The file was modified etc/options (diff)
The file was modified src/Pure/Thy/presentation.scala (diff)
Changeset 74731:161e84e6b40a by wenzelm:
just one cache, via HTML_Context, via Sessions.Store or Session;
The file was modified src/Pure/PIDE/session.scala (diff)
The file was modified src/Pure/PIDE/xml.scala (diff)
The file was modified src/Pure/Thy/presentation.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/build_job.scala (diff)
The file was modified src/Pure/term.scala (diff)
Changeset 74730:25f5f1fa31bb by paulson:
merged
Changeset 74729:64b3d8d9bd10 by paulson _lp15@cam.ac.uk_:
new lemmas about convex, concave functions, + tidying
The file was modified src/HOL/Analysis/Convex.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)