equal
deleted
inserted
replaced
266 |
266 |
267 |
267 |
268 local |
268 local |
269 |
269 |
270 val refine_witness = |
270 val refine_witness = |
271 Proof.refine (Method.Basic (K (Method.RAW_METHOD |
271 Proof.refine (Method.Basic (K (RAW_METHOD |
272 (K (ALLGOALS |
272 (K (ALLGOALS |
273 (CONJUNCTS (ALLGOALS |
273 (CONJUNCTS (ALLGOALS |
274 (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none)); |
274 (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none)); |
275 |
275 |
276 fun gen_witness_proof proof after_qed wit_propss eq_props = |
276 fun gen_witness_proof proof after_qed wit_propss eq_props = |