src/HOL/Tools/SMT/smtlib_interface.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39298 5aefb5bc8a93
     1.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -162,12 +162,12 @@
     1.4    | conn @{const_name HOL.conj} = SOME "and"
     1.5    | conn @{const_name HOL.disj} = SOME "or"
     1.6    | conn @{const_name HOL.implies} = SOME "implies"
     1.7 -  | conn @{const_name "op ="} = SOME "iff"
     1.8 +  | conn @{const_name HOL.eq} = SOME "iff"
     1.9    | conn @{const_name If} = SOME "if_then_else"
    1.10    | conn _ = NONE
    1.11  
    1.12  fun pred @{const_name distinct} _ = SOME "distinct"
    1.13 -  | pred @{const_name "op ="} _ = SOME "="
    1.14 +  | pred @{const_name HOL.eq} _ = SOME "="
    1.15    | pred @{const_name term_eq} _ = SOME "="
    1.16    | pred @{const_name less} T = if_int_type T "<"
    1.17    | pred @{const_name less_eq} T = if_int_type T "<="