Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. systematic access to command ids;
  3. more robust: Pure entities may lack id;
  4. merged
  5. tagged 21 theories in the Analysis library for the manual
  6. tuned output;
  7. Export.Provider for "isabelle dump" output_dir;
  8. retain original id, which is command_id/exec_id for PIDE; tuned;
  9. tuned signature;
  10. tuned;
  11. tuned signature;
  12. clarified ML_environment: ML_write_global requires "Isabelle";
  13. clarified signature: do not expose internal operation;
Changeset 68837:99f0aee4adbd by wenzelm:
merged
Changeset 68836:cf52379c0776 by wenzelm:
systematic access to command ids;
The file was modified src/Pure/PIDE/document.scala (diff)
Changeset 68835:2e59da922630 by wenzelm:
more robust: Pure entities may lack id;
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 68834:43334463428a by angeliki koutsoukouargyraki _ak2110@cam.ac.uk_:
merged
Changeset 68833:fde093888c16 by angeliki koutsoukouargyraki _ak2110@cam.ac.uk_:
tagged 21 theories in the Analysis library for the manual
The file was modified src/HOL/Analysis/Arcwise_Connected.thy (diff)
The file was modified src/HOL/Analysis/Binary_Product_Measure.thy (diff)
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
The file was modified src/HOL/Analysis/Borel_Space.thy (diff)
The file was modified src/HOL/Analysis/Caratheodory.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Space.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Cross3.thy (diff)
The file was modified src/HOL/Analysis/Determinants.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Finite_Product_Measure.thy (diff)
The file was modified src/HOL/Analysis/Function_Topology.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.thy (diff)
The file was modified src/HOL/Analysis/Operator_Norm.thy (diff)
The file was modified src/HOL/Analysis/Ordered_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Poly_Roots.thy (diff)
The file was modified src/HOL/Analysis/Polytope.thy (diff)
The file was modified src/HOL/Analysis/Vitali_Covering_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy (diff)
Changeset 68832:9b9fc9ea9dd1 by wenzelm:
tuned output;
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 68831:a6c69599ab99 by wenzelm:
Export.Provider for "isabelle dump" output_dir;
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 68830:44ec6fdaacf8 by wenzelm:
retain original id, which is command_id/exec_id for PIDE;<br>tuned;
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 68829:1a4fa494a4a8 by wenzelm:
tuned signature;
The file was modified src/Pure/General/position.ML (diff)
The file was modified src/Pure/PIDE/active.ML (diff)
Changeset 68828:7030922e91a1 by wenzelm:
tuned;
The file was modified src/HOL/Real_Asymp/real_asymp_diag.ML (diff)
Changeset 68827:1286ca9dfd26 by wenzelm:
tuned signature;
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/config.ML (diff)
Changeset 68826:deefe5837120 by wenzelm:
clarified ML_environment: ML_write_global requires &quot;Isabelle&quot;;
The file was modified src/Pure/Pure.thy (diff)
Changeset 68825:8207c67d9ef4 by wenzelm:
clarified signature: do not expose internal operation;
The file was modified src/HOL/TPTP/TPTP_Proof_Reconstruction.thy (diff)
The file was modified src/Pure/tactic.ML (diff)