equal
deleted
inserted
replaced
75 | string_for_connective AIff = "<=>" |
75 | string_for_connective AIff = "<=>" |
76 | string_for_connective ANotIff = "<~>" |
76 | string_for_connective ANotIff = "<~>" |
77 fun string_for_formula (AQuant (q, xs, phi)) = |
77 fun string_for_formula (AQuant (q, xs, phi)) = |
78 string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^ |
78 string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^ |
79 string_for_formula phi |
79 string_for_formula phi |
|
80 | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) = |
|
81 space_implode " != " (map string_for_term ts) |
80 | string_for_formula (AConn (c, [phi])) = |
82 | string_for_formula (AConn (c, [phi])) = |
81 string_for_connective c ^ " " ^ string_for_formula phi |
83 string_for_connective c ^ " " ^ string_for_formula phi |
82 | string_for_formula (AConn (c, phis)) = |
84 | string_for_formula (AConn (c, phis)) = |
83 "(" ^ space_implode (" " ^ string_for_connective c ^ " ") |
85 "(" ^ space_implode (" " ^ string_for_connective c ^ " ") |
84 (map string_for_formula phis) ^ ")" |
86 (map string_for_formula phis) ^ ")" |