equal
deleted
inserted
replaced
30 |
30 |
31 val (_, make_thm_cterm) = |
31 val (_, make_thm_cterm) = |
32 Context.>>> |
32 Context.>>> |
33 (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", @{here}), I))); |
33 (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", @{here}), I))); |
34 |
34 |
35 fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop); |
35 fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop); |
36 |
36 |
37 |
37 |
38 (* cheat_tac *) |
38 (* cheat_tac *) |
39 |
39 |
40 fun cheat_tac ctxt i st = |
40 fun cheat_tac ctxt i st = |