equal
deleted
inserted
replaced
113 handle TYPE _ => @{prop True} |
113 handle TYPE _ => @{prop True} |
114 end |
114 end |
115 |
115 |
116 fun all_non_tautological_facts_of thy css_table = |
116 fun all_non_tautological_facts_of thy css_table = |
117 Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table |
117 Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table |
118 |> filter_out (Sledgehammer_MaSh.is_likely_tautology_or_too_meta o snd) |
118 |> filter_out (Sledgehammer_Fact.is_likely_tautology_or_too_meta o snd) |
119 |
119 |
120 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name = |
120 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name = |
121 let |
121 let |
122 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
122 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt |
123 val type_enc = |
123 val type_enc = |