# HG changeset patch
# User wenzelm
# Date 1566041080 -7200
# Node ID 61414c54a70c0a235618a0b053657057d15c7fe2
# Parent  86692888c313aa18a678b43e861c2d88272729cb
tuned comments;

diff -r 86692888c313 -r 61414c54a70c src/Pure/skip_proof.ML
--- a/src/Pure/skip_proof.ML	Sat Aug 17 13:17:40 2019 +0200
+++ b/src/Pure/skip_proof.ML	Sat Aug 17 13:24:40 2019 +0200
@@ -32,7 +32,7 @@
 fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop);
 
 
-(* cheat_tac *)
+(* cheat_tac -- 'sorry' *)
 
 fun cheat_tac ctxt = SUBGOAL (fn (goal, i) =>
   let