Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. expose derivations more thoroughly, notably for locale/class reasoning;
  2. clarified errors;
  3. determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
  4. more operations;
  5. tuned whitespace;
  6. more robust;
  7. clarified modules;
  8. clarified signature -- more options;
  9. merged
  10. moved line segments to Convex_Euclidean_Space
Changeset 71017:c85efa2be619 by wenzelm:
expose derivations more thoroughly, notably for locale/class reasoning;
The file was modified src/Pure/Isar/class_declaration.ML (diff)
The file was modified src/Pure/Isar/element.ML (diff)
The file was modified src/Pure/Isar/expression.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 71016:b05d78bfc67c by wenzelm:
clarified errors;
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 71015:bb49abc2ecbb by wenzelm:
determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
The file was modified src/Pure/thm_deps.ML (diff)
Changeset 71014:58022ee70b35 by wenzelm:
more operations;
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 71013:bfa1017b4553 by wenzelm:
tuned whitespace;
The file was modified src/HOL/Lattices.thy (diff)
Changeset 71012:73f14e0b7151 by wenzelm:
more robust;
The file was modified src/Pure/thm.ML (diff)
Changeset 71011:2c96e48027eb by wenzelm:
clarified modules;
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 71010:be689b7d81fd by wenzelm:
clarified signature -- more options;
The file was modified src/Pure/Proof/proof_syntax.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 71009:bb403cb94db2 by paulson:
merged
Changeset 71008:e892f7a1fd83 by paulson _lp15@cam.ac.uk_:
moved line segments to Convex_Euclidean_Space
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)