equal
deleted
inserted
replaced
119 val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
119 val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
120 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
120 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
121 val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") |
121 val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") |
122 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths |
122 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths |
123 val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) |
123 val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) |
124 val type_enc = type_enc_from_string Unsound type_enc |
124 val type_enc = type_enc_from_string Sound type_enc |
125 val (sym_tab, axioms, old_skolems) = |
125 val (sym_tab, axioms, old_skolems) = |
126 prepare_metis_problem ctxt type_enc cls ths |
126 prepare_metis_problem ctxt type_enc cls ths |
127 fun get_isa_thm mth Isa_Reflexive_or_Trivial = |
127 fun get_isa_thm mth Isa_Reflexive_or_Trivial = |
128 reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth |
128 reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth |
129 | get_isa_thm _ (Isa_Raw ith) = ith |
129 | get_isa_thm _ (Isa_Raw ith) = ith |