src/HOL/Tools/ATP/atp_proof.ML
changeset 73972 b304285fd800
parent 73971 96a05b8462f9
child 74006 1a0a536b8aaf
equal deleted inserted replaced
73971:96a05b8462f9 73972:b304285fd800
   474   | role_of_tptp_string "plain" = Plain
   474   | role_of_tptp_string "plain" = Plain
   475   | role_of_tptp_string "type" = Type_Role
   475   | role_of_tptp_string "type" = Type_Role
   476   | role_of_tptp_string _ = Unknown
   476   | role_of_tptp_string _ = Unknown
   477 
   477 
   478 val tptp_binary_ops =
   478 val tptp_binary_ops =
   479   [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff,
   479   [tptp_and, tptp_or, tptp_implies, tptp_iff, tptp_if, tptp_equal, tptp_not_equal, tptp_not_and,
   480    tptp_equal, tptp_not_equal, tptp_app]
   480    tptp_not_or, tptp_not_iff, tptp_app]
   481 
   481 
   482 fun parse_one_in_list xs =
   482 fun parse_one_in_list xs =
   483   foldl1 (op ||) (map Scan.this_string xs)
   483   foldl1 (op ||) (map Scan.this_string xs)
   484 
   484 
   485 fun parse_binary_op x =
   485 fun parse_binary_op x =