equal
deleted
inserted
replaced
8 "sum" > "sum_def" |
8 "sum" > "sum_def" |
9 |
9 |
10 const_maps |
10 const_maps |
11 "sup" > "HOL4Real.real.sup" |
11 "sup" > "HOL4Real.real.sup" |
12 "sum" > "HOL4Real.real.sum" |
12 "sum" > "HOL4Real.real.sum" |
13 "real_sub" > "op -" :: "real => real => real" |
13 "real_sub" > "HOL.minus" :: "real => real => real" |
14 "real_of_num" > "RealDef.real" :: "nat => real" |
14 "real_of_num" > "RealDef.real" :: "nat => real" |
15 "real_lte" > "op <=" :: "real => real => bool" |
15 "real_lte" > "op <=" :: "real => real => bool" |
16 "real_gt" > "HOL4Compat.real_gt" |
16 "real_gt" > "HOL4Compat.real_gt" |
17 "real_ge" > "HOL4Compat.real_ge" |
17 "real_ge" > "HOL4Compat.real_ge" |
18 "pow" > "Nat.power" :: "real => nat => real" |
18 "pow" > "Nat.power" :: "real => nat => real" |