Summary
- uniform use of original theory;
- implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof;
The file was modified | src/Pure/Isar/toplevel.ML (diff) |
The file was modified | src/Pure/Isar/proof.ML (diff) |
The file was modified | src/Pure/Isar/toplevel.ML (diff) |
The file was modified | src/Pure/Isar/proof.ML (diff) |