Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. tuned proofs;
  2. re-use name space serial as unique (!) id;
  3. clarified;
  4. information about proof outline with cases (sendback);
  5. tuned signature;
  6. more operations;
  7. singleton result for 'proof' command (without backtracking), e.g. relevant for well-defined output;
  8. unused;
  9. more structured edit, including indentation;
  10. clarified markup;
Changeset 63516:76492eaf3dc1 by wenzelm:
tuned proofs;
The file was modified src/HOL/Library/Convex.thy (diff)
The file was modified src/HOL/Library/Discrete.thy (diff)
Changeset 63515:6c46a1e786da by wenzelm:
re-use name space serial as unique (!) id;
The file was modified src/Pure/Isar/proof_context.ML (diff)
Changeset 63514:d4d3df24f536 by wenzelm:
clarified;
The file was modified src/Pure/Isar/proof_context.ML (diff)
Changeset 63513:9f8d06f23c09 by wenzelm:
information about proof outline with cases (sendback);
The file was modified NEWS (diff)
The file was modified src/Pure/Isar/proof_context.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
Changeset 63512:1c7b1e294fb5 by wenzelm:
tuned signature;
The file was modified src/Pure/Isar/rule_cases.ML (diff)
Changeset 63511:1c2c045decb3 by wenzelm:
more operations;
The file was modified src/Pure/General/table.ML (diff)
Changeset 63510:0fc8be2f8176 by wenzelm:
singleton result for 'proof' command (without backtracking), e.g. relevant for well-defined output;
The file was modified src/Pure/Pure.thy (diff)
Changeset 63509:3b9ab054a356 by wenzelm:
unused;
The file was modified src/Pure/Isar/proof_context.ML (diff)
Changeset 63508:348599644887 by wenzelm:
more structured edit, including indentation;
The file was modified src/Tools/jEdit/src/active.scala (diff)
The file was modified src/Tools/jEdit/src/isabelle.scala (diff)
Changeset 63507:79122bdd4404 by wenzelm:
clarified markup;
The file was modified src/HOL/Library/Sum_of_Squares/sos_wrapper.ML (diff)
The file was modified src/HOL/Statespace/StateSpaceEx.thy (diff)