Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. more robust, notably for open_proof of unnamed derivation;
  2. tuned comments;
  3. NEWS;
  4. more accurate proposition for cheat_tac (command 'sorry');
  5. added command 'thm_oracles';
  6. clarified type for recorded oracles;
  7. unused;
  8. clarified signature;
  9. clarified modules;
  10. clarified lookup operations: more scalable for multiple retrieval;
  11. clarified signature;
Changeset 70564:2c7c8be65b7d by wenzelm:
more robust, notably for open_proof of unnamed derivation;
The file was modified src/Pure/Isar/runtime.ML
The file was modified src/Pure/proofterm.ML
The file was modified src/Pure/thm.ML
Changeset 70563:61414c54a70c by wenzelm:
tuned comments;
The file was modified src/Pure/skip_proof.ML
Changeset 70562:86692888c313 by wenzelm:
NEWS;
The file was modified NEWS
Changeset 70561:0c1b08d0b1fe by wenzelm:
more accurate proposition for cheat_tac (command 'sorry');
The file was modified src/Pure/skip_proof.ML
Changeset 70560:7714971a58b5 by wenzelm:
added command 'thm_oracles';
The file was modified src/Doc/Isar_Ref/Proof.thy
The file was modified src/Doc/Isar_Ref/Spec.thy
The file was modified src/Pure/Pure.thy
The file was modified src/Pure/Thy/thm_deps.ML
The file was modified src/Pure/thm.ML
Changeset 70559:c92443e8d724 by wenzelm:
clarified type for recorded oracles;
The file was modified src/Pure/proofterm.ML
The file was modified src/Pure/term.scala
The file was modified src/Pure/term_xml.scala
Changeset 70558:36e41783bb6e by wenzelm:
unused;
The file was modified src/Pure/thm.ML
Changeset 70557:5d6e9c65ea67 by wenzelm:
clarified signature;
The file was modified src/Pure/Thy/thm_deps.ML
The file was modified src/Pure/proofterm.ML
Changeset 70556:038ed9b76c2b by wenzelm:
clarified modules;
The file was addedsrc/Pure/Thy/thm_deps.ML
The file was modified src/Pure/ROOT.ML
The file was removedsrc/Pure/Tools/thm_deps.ML
Changeset 70555:c1fde53e5e82 by wenzelm:
clarified lookup operations: more scalable for multiple retrieval;
The file was modified src/Pure/global_theory.ML
Changeset 70554:10d41bf28b92 by wenzelm:
clarified signature;
The file was modified src/Pure/proofterm.ML
The file was modified src/Pure/term.scala
The file was modified src/Pure/thm.ML