equal
deleted
inserted
replaced
71 let val ts = map (hol_term_from_fo_term iotaT) us in |
71 let val ts = map (hol_term_from_fo_term iotaT) us in |
72 list_comb ((case x of |
72 list_comb ((case x of |
73 "$true" => @{const_name True} |
73 "$true" => @{const_name True} |
74 | "$false" => @{const_name False} |
74 | "$false" => @{const_name False} |
75 | "=" => @{const_name HOL.eq} |
75 | "=" => @{const_name HOL.eq} |
|
76 | "equal" => @{const_name HOL.eq} |
76 | _ => x, map fastype_of ts ---> res_T) |
77 | _ => x, map fastype_of ts ---> res_T) |
77 |> (if is_variable x then Free else Const), ts) |
78 |> (if is_variable x then Free else Const), ts) |
78 end |
79 end |
79 |
80 |
80 fun hol_prop_from_formula phi = |
81 fun hol_prop_from_formula phi = |