equal
deleted
inserted
replaced
24 |
24 |
25 |
25 |
26 (* oracle setup *) |
26 (* oracle setup *) |
27 |
27 |
28 val (_, make_thm_cterm) = |
28 val (_, make_thm_cterm) = |
29 Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "skip_proof", I))); |
29 Context.>>> |
|
30 (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", @{here}), I))); |
30 |
31 |
31 fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop); |
32 fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop); |
32 |
33 |
33 |
34 |
34 (* cheat_tac *) |
35 (* cheat_tac *) |