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