135 val datatype_methods = [Simp_Method, Simp_Size_Method] |
135 val datatype_methods = [Simp_Method, Simp_Size_Method] |
136 val systematic_methods = |
136 val systematic_methods = |
137 basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ |
137 basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ |
138 [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)] |
138 [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)] |
139 val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods |
139 val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods |
140 val skolem_methods = basic_systematic_methods @ [Auto_Choice_Method] |
140 val skolem_methods = basic_systematic_methods @ [Skolem_Method] |
141 |
141 |
142 fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params |
142 fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params |
143 (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = |
143 (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = |
144 let |
144 let |
145 val _ = if debug then Output.urgent_message "Constructing Isar proof..." else () |
145 val _ = if debug then Output.urgent_message "Constructing Isar proof..." else () |