Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. prefer infix operations;
  2. structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
  3. proper signature;
  4. tuned signature;
  5. tuned;
  6. tuned signature;
  7. proper type; tuned;
  8. careful export of type-dependent functions, without losing their special status;
  9. clarified modules;
  10. clarified modules;
Changeset 62826:eb94e570c1a4 by wenzelm:
prefer infix operations;
The file was modified src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Nitpick/kodkod.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/async_manager_legacy.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_util.ML (diff)
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/mailbox.ML (diff)
The file was modified src/Pure/Concurrent/multithreading.ML (diff)
The file was modified src/Pure/Concurrent/task_queue.ML (diff)
The file was modified src/Pure/Concurrent/timeout.ML (diff)
The file was modified src/Pure/General/timing.ML (diff)
The file was modified src/Pure/Isar/toplevel.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/Tools/build.ML (diff)
Changeset 62825:e6e80a8bf624 by wenzelm:
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
The file was modified src/Pure/ML/ml_heap.ML (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 62824:3498c66b5e55 by wenzelm:
proper signature;
The file was modified src/Pure/ML/ml_profiling.ML (diff)
Changeset 62823:751bcf0473a7 by wenzelm:
tuned signature;
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/General/pretty.ML (diff)
The file was modified src/Pure/ML/ml_pervasive.ML (diff)
The file was modified src/Pure/ML/ml_pretty.ML (diff)
Changeset 62822:941b6a48ff67 by wenzelm:
tuned;
The file was modified src/Pure/ML/ml_debugger.ML (diff)
Changeset 62821:48c24d0b6d85 by wenzelm:
tuned signature;
The file was modified src/Pure/General/exn.ML (diff)
The file was modified src/Pure/Isar/runtime.ML (diff)
The file was modified src/Pure/ML/exn_debugger.ML (diff)
The file was modified src/Pure/ML/exn_properties.ML (diff)
The file was modified src/Pure/ML/ml_compiler.ML (diff)
The file was modified src/Pure/ML/ml_compiler0.ML (diff)
The file was modified src/Pure/ML/ml_debugger.ML (diff)
The file was modified src/Pure/Tools/debugger.ML (diff)
Changeset 62820:5c678ee5d34a by wenzelm:
proper type;<br>tuned;
The file was modified src/Pure/General/pretty.ML (diff)
The file was modified src/Pure/General/pretty.scala (diff)
Changeset 62819:d3ff367a16a0 by wenzelm:
careful export of type-dependent functions, without losing their special status;
The file was modified Admin/polyml/future/ROOT.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/synchronized.ML (diff)
The file was modified src/Pure/Concurrent/task_queue.ML (diff)
The file was modified src/Pure/General/binding.ML (diff)
The file was modified src/Pure/General/linear_set.ML (diff)
The file was modified src/Pure/General/path.ML (diff)
The file was modified src/Pure/General/pretty.ML (diff)
The file was modified src/Pure/General/sha1.ML (diff)
The file was modified src/Pure/General/table.ML (diff)
The file was modified src/Pure/Isar/proof.ML (diff)
The file was modified src/Pure/Isar/runtime.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/ML/ml_compiler0.ML (diff)
The file was modified src/Pure/ML/ml_debugger.ML (diff)
The file was modified src/Pure/ML/ml_name_space.ML (diff)
The file was modified src/Pure/ML/ml_pp.ML (diff)
The file was modified src/Pure/ML/ml_pretty.ML (diff)
The file was modified src/Pure/ML/ml_syntax.ML (diff)
The file was modified src/Pure/PIDE/xml.ML (diff)
The file was modified src/Pure/Syntax/ast.ML (diff)
The file was modified src/Pure/Syntax/lexicon.ML (diff)
The file was modified src/Pure/context.ML (diff)
The file was modified src/Pure/morphism.ML (diff)
Changeset 62818:2733b240bfea by wenzelm:
clarified modules;
The file was addedsrc/Pure/ML/ml_pervasive.ML
The file was modified src/Pure/Concurrent/unsynchronized.ML (diff)
The file was modified src/Pure/ROOT (diff)
The file was modified src/Pure/ROOT.ML (diff)
Changeset 62817:744bfd770123 by wenzelm:
clarified modules;
The file was addedsrc/Pure/ML/ml_compiler1.ML
The file was addedsrc/Pure/ML/ml_compiler2.ML
The file was modified src/Pure/ML/ml_compiler0.ML (diff)
The file was modified src/Pure/ROOT (diff)
The file was modified src/Pure/ROOT.ML (diff)