Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned
  2. always export Pure proofs;
  3. clarified 'thm_deps' command;
  4. more compact: avoid pointless PThm rudiments;
  5. clarified signature: prefer total operations;
Changeset 70607:b044a06ad0d6 by nipkow:
tuned
The file was modified src/HOL/Data_Structures/Binomial_Heap.thy (diff)
Changeset 70606:4f4ede010687 by wenzelm:
always export Pure proofs;
The file was modified src/Pure/ROOT (diff)
Changeset 70605:048cf2096186 by wenzelm:
clarified 'thm_deps' command;
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Outer_Syntax.thy (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/thm_deps.ML (diff)
Changeset 70604:8088cf2576f3 by wenzelm:
more compact: avoid pointless PThm rudiments;
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70603:706dac15554b by wenzelm:
clarified signature: prefer total operations;
The file was modified src/Pure/Isar/runtime.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)