Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified error;
  2. removed somewhat pointless warning;
  3. uniform use of original theory;
  4. implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof;
  5. avoid smt proofs in distribution
Changeset 67164:39f57f0757f1 by wenzelm:
clarified error;
The file was modified src/Pure/Thy/thy_header.ML (diff)
The file was modified src/Pure/Thy/thy_header.scala (diff)
Changeset 67163:257bcd20eeec by wenzelm:
removed somewhat pointless warning;
The file was modified src/Pure/Thy/thy_info.ML (diff)
Changeset 67162:0050cd50936d by wenzelm:
uniform use of original theory;
The file was modified src/Pure/Isar/toplevel.ML (diff)
Changeset 67161:b762ed417ed9 by wenzelm:
implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof;
The file was modified src/Pure/Isar/proof.ML (diff)
Changeset 67160:f37bf261bdf6 by haftmann:
avoid smt proofs in distribution
The file was modified src/HOL/Word/Bit_Representation.thy (diff)
The file was modified src/HOL/Word/Misc_Numeric.thy (diff)