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.>>> |
29 Theory.setup_result (Thm.add_oracle (Binding.make ("skip_proof", \<^here>), I)); |
30 (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", \<^here>), I))); |
|
31 |
30 |
32 fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop); |
31 fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop); |
33 |
32 |
34 |
33 |
35 (* cheat_tac -- 'sorry' *) |
34 (* cheat_tac -- 'sorry' *) |