src/HOL/Tools/ATP/atp_problem.ML
changeset 74393 b9837b07684d
parent 74339 a5bab59d580b
child 74433 304f22435bc7
equal deleted inserted replaced
74392:94c27a7a0d39 74393:b9837b07684d
   498               val definition = s' ^ " := " ^ of_term t1
   498               val definition = s' ^ " := " ^ of_term t1
   499               val usage = of_term tm
   499               val usage = of_term tm
   500             in
   500             in
   501             s ^ "(" ^ declaration ^ ", " ^ definition ^ ", " ^ usage ^ ")"
   501             s ^ "(" ^ declaration ^ ", " ^ definition ^ ", " ^ usage ^ ")"
   502             end
   502             end
       
   503         | _ => app ())
       
   504       else if s = tptp_ite then
       
   505         (case ts of
       
   506           [t1, t2, t3] => s ^ "(" ^ of_term t1 ^ ", " ^ of_term t2 ^ ", " ^ of_term t3 ^ ")"
   503         | _ => app ())
   507         | _ => app ())
   504       else if s = tptp_choice then
   508       else if s = tptp_choice then
   505         (case ts of
   509         (case ts of
   506           [AAbs (((s', ty), tm), args)] =>
   510           [AAbs (((s', ty), tm), args)] =>
   507           (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always applied to an
   511           (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always applied to an