Skip to content
Success

Changes

Summary

  1. uniform use of original theory;
  2. implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof;
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)