equal
deleted
inserted
replaced
243 fun pretty_statement ctxt kind raw_th = |
243 fun pretty_statement ctxt kind raw_th = |
244 let |
244 let |
245 val thy = ProofContext.theory_of ctxt; |
245 val thy = ProofContext.theory_of ctxt; |
246 val cert = Thm.cterm_of thy; |
246 val cert = Thm.cterm_of thy; |
247 |
247 |
248 val th = norm_hhf raw_th; |
248 val th = MetaSimplifier.norm_hhf raw_th; |
249 val is_elim = ObjectLogic.is_elim th; |
249 val is_elim = ObjectLogic.is_elim th; |
250 |
250 |
251 val ((_, [th']), ctxt') = Variable.import true [th] ctxt; |
251 val ((_, [th']), ctxt') = Variable.import true [th] ctxt; |
252 val prop = Thm.prop_of th'; |
252 val prop = Thm.prop_of th'; |
253 val (prems, concl) = Logic.strip_horn prop; |
253 val (prems, concl) = Logic.strip_horn prop; |
289 |
289 |
290 fun prove_witness ctxt t tac = |
290 fun prove_witness ctxt t tac = |
291 Witness (t, Goal.prove ctxt [] [] (Logic.protect t) (fn _ => |
291 Witness (t, Goal.prove ctxt [] [] (Logic.protect t) (fn _ => |
292 Tactic.rtac Drule.protectI 1 THEN tac)); |
292 Tactic.rtac Drule.protectI 1 THEN tac)); |
293 |
293 |
294 fun conclude_witness (Witness (_, th)) = norm_hhf (Goal.conclude th); |
294 fun conclude_witness (Witness (_, th)) = MetaSimplifier.norm_hhf_protect (Goal.conclude th); |
295 |
295 |
296 val mark_witness = Logic.protect; |
296 val mark_witness = Logic.protect; |
297 |
297 |
298 fun make_witness t th = Witness (t, th); |
298 fun make_witness t th = Witness (t, th); |
299 fun dest_witness (Witness w) = w; |
299 fun dest_witness (Witness w) = w; |