equal
deleted
inserted
replaced
166 fun some isa = |
166 fun some isa = |
167 SOME (phi |> metis_literals_from_atp type_enc |
167 SOME (phi |> metis_literals_from_atp type_enc |
168 |> Metis_LiteralSet.fromList |
168 |> Metis_LiteralSet.fromList |
169 |> Metis_Thm.axiom, isa) |
169 |> Metis_Thm.axiom, isa) |
170 in |
170 in |
171 if ident = type_tag_idempotence_helper_name orelse |
171 if String.isPrefix tags_sym_formula_prefix ident then |
172 String.isPrefix tags_sym_formula_prefix ident then |
|
173 Isa_Reflexive_or_Trivial |> some |
172 Isa_Reflexive_or_Trivial |> some |
174 else if String.isPrefix conjecture_prefix ident then |
173 else if String.isPrefix conjecture_prefix ident then |
175 NONE |
174 NONE |
176 else if String.isPrefix helper_prefix ident then |
175 else if String.isPrefix helper_prefix ident then |
177 case (String.isSuffix typed_helper_suffix ident, |
176 case (String.isSuffix typed_helper_suffix ident, |