src/HOL/Import/hol4rews.ML
changeset 38864 4abe644fcea5
parent 38786 e46e7a9cb622
child 39159 0dec18004e75
     1.1 --- a/src/HOL/Import/hol4rews.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -627,7 +627,7 @@
     1.4          thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool}
     1.5              |> add_hol4_type_mapping "min" "fun" false "fun"
     1.6              |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
     1.7 -            |> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
     1.8 +            |> add_hol4_const_mapping "min" "=" false @{const_name HOL.eq}
     1.9              |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
    1.10              |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
    1.11  in