Summary
- expose derivations more thoroughly, notably for locale/class reasoning;
- clarified errors;
- determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
- more operations;
- tuned whitespace;
- more robust;
- clarified modules;
- clarified signature -- more options;
- merged
- moved line segments to Convex_Euclidean_Space
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) |
The file was modified | src/Pure/Thy/export_theory.scala (diff) |
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) |
The file was modified | src/Pure/Thy/export.scala (diff) |
The file was modified | src/HOL/Lattices.thy (diff) |
The file was modified | src/Pure/thm.ML (diff) |
The file was modified | src/Pure/more_thm.ML (diff) |
The file was modified | src/Pure/thm.ML (diff) |
The file was modified | src/Pure/Proof/proof_syntax.ML (diff) |
The file was modified | src/Pure/proofterm.ML (diff) |
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) |