equal
deleted
inserted
replaced
119 let val ctxt = Config.put SMT2_Config.verbose false ctxt in |
119 let val ctxt = Config.put SMT2_Config.verbose false ctxt in |
120 SMT2_Solver.smt2_tac ctxt global_facts |
120 SMT2_Solver.smt2_tac ctxt global_facts |
121 end |
121 end |
122 | Simp_Method => Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps global_facts) |
122 | Simp_Method => Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps global_facts) |
123 | Simp_Size_Method => |
123 | Simp_Size_Method => |
124 Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps @{thms size_ne_size_imp_ne}) |
124 Simplifier.asm_full_simp_tac |
|
125 (silence_methods ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts)) |
125 | _ => |
126 | _ => |
126 Method.insert_tac global_facts THEN' |
127 Method.insert_tac global_facts THEN' |
127 (case meth of |
128 (case meth of |
128 SATx_Method => SAT.satx_tac ctxt |
129 SATx_Method => SAT.satx_tac ctxt |
129 | Blast_Method => blast_tac ctxt |
130 | Blast_Method => blast_tac ctxt |