tuned comments;
authorwenzelm
Sat, 17 Aug 2019 13:24:40 +0200
changeset 70563 61414c54a70c
parent 70562 86692888c313
child 70564 2c7c8be65b7d
tuned comments;
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