equal
deleted
inserted
replaced
303 fun transfer_witness thy (Witness (t, th)) = Witness (t, Thm.transfer thy th); |
303 fun transfer_witness thy (Witness (t, th)) = Witness (t, Thm.transfer thy th); |
304 |
304 |
305 val refine_witness = |
305 val refine_witness = |
306 Proof.refine (Method.Basic (K (Method.RAW_METHOD |
306 Proof.refine (Method.Basic (K (Method.RAW_METHOD |
307 (K (ALLGOALS |
307 (K (ALLGOALS |
308 (PRECISE_CONJUNCTS ~1 (ALLGOALS |
308 (CONJUNCTS (ALLGOALS |
309 (PRECISE_CONJUNCTS ~1 (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none)); |
309 (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none)); |
310 |
310 |
311 fun pretty_witness ctxt witn = |
311 fun pretty_witness ctxt witn = |
312 let val prt_term = Pretty.quote o ProofContext.pretty_term ctxt in |
312 let val prt_term = Pretty.quote o ProofContext.pretty_term ctxt in |
313 Pretty.block (prt_term (witness_prop witn) :: |
313 Pretty.block (prt_term (witness_prop witn) :: |
314 (if ! show_hyps then [Pretty.brk 2, Pretty.list "[" "]" |
314 (if ! show_hyps then [Pretty.brk 2, Pretty.list "[" "]" |