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" > "HOL.minus_class.minus" :: "real => real => real" |
13 "real_sub" > "Algebras.minus" :: "real => real => real" |
14 "real_of_num" > "RealDef.real" :: "nat => real" |
14 "real_of_num" > "RealDef.real" :: "nat => real" |
15 "real_lte" > "HOL.ord_class.less_eq" :: "real => real => bool" |
15 "real_lte" > "Algebras.less_eq" :: "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" > "Power.power_class.power" :: "real => nat => real" |
18 "pow" > "Power.power_class.power" :: "real => nat => real" |
19 "abs" > "HOL.minus_class.abs" :: "real => real" |
19 "abs" > "Algebras.abs" :: "real => real" |
20 "/" > "HOL.divides_class.divide" :: "real => real => real" |
20 "/" > "Algebras.divide" :: "real => real => real" |
21 |
21 |
22 thm_maps |
22 thm_maps |
23 "sup_def" > "HOL4Real.real.sup_def" |
23 "sup_def" > "HOL4Real.real.sup_def" |
24 "sup" > "HOL4Real.real.sup" |
24 "sup" > "HOL4Real.real.sup" |
25 "sumc" > "HOL4Real.real.sumc" |
25 "sumc" > "HOL4Real.real.sumc" |