Entry	Value
Package Name	real-def
Count	10
Theorems	real_abs : !x. abs x = (if &0 <= x then x else --x) real_div : !x y. ~(y = &0) ==> x / y = x * inv y real_ge : !x y. x >= y <=> y <= x real_gt : !x y. x > y <=> y < x real_lt : !x y. x < y <=> ~(y <= x) real_max : !m n. max m n = (if m <= n then n else m) real_min : !m n. min m n = (if m <= n then m else n) real_pow_suc : !x n. x pow SUC n = x * x pow n real_pow_zero : !x. x pow 0 = &1 real_sub : !x y. x - y = x + --y

Back to main package page