equal
deleted
inserted
replaced
47 ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] ORELSE' |
47 ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] ORELSE' |
48 blast_tac ctxt)) |
48 blast_tac ctxt)) |
49 *} |
49 *} |
50 |
50 |
51 method_setup moura = {* |
51 method_setup moura = {* |
52 Scan.succeed (SIMPLE_METHOD' o moura_tac) |
52 Scan.succeed (SIMPLE_METHOD' o moura_tac) |
53 *} "solve skolemization goals, especially those arising from Z3 proofs" |
53 *} "solve skolemization goals, especially those arising from Z3 proofs" |
54 |
54 |
55 hide_fact (open) choices bchoices |
55 hide_fact (open) choices bchoices |
56 |
56 |
57 |
57 |