author | desharna |
Mon, 16 Aug 2021 23:07:01 +0200 | |
changeset 74154 | 62b0577123a5 |
parent 74153 | 46f66e821f5c (diff) |
parent 74152 | 069f6b2c5a07 (current diff) |
child 74155 | 0faa68dedce5 |
child 74190 | 9a1796acd0a4 |
--- a/src/HOL/Tools/ATP/atp_problem.ML Mon Aug 16 11:49:39 2021 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Aug 16 23:07:01 2021 +0200 @@ -501,6 +501,10 @@ s ^ "(" ^ declaration ^ ", " ^ definition ^ ", " ^ usage ^ ")" end | _ => app ()) + else if s = tptp_ite then + (case ts of + [t1, t2, t3] => s ^ "(" ^ of_term t1 ^ ", " ^ of_term t2 ^ ", " ^ of_term t3 ^ ")" + | _ => app ()) else if s = tptp_choice then (case ts of [AAbs (((s', ty), tm), args)] =>