REAL_RING : term -> thm
# REAL_RING `y * (c * x + d) = a * x + b ==> x * (c * y - a) = b - d * y`;; 2 basis elements and 0 critical pairs val it : thm = |- y * (c * x + d) = a * x + b ==> x * (c * y - a) = b - d * y
# REAL_RING `p = (&3 * a1 - a2 pow 2) / &3 /\ q = (&9 * a1 * a2 - &27 * a0 - &2 * a2 pow 3) / &27 /\ z = x - a2 / &3 /\ x * w = w pow 2 - p / &3 /\ ~(p = &0) ==> (z pow 3 + a2 * z pow 2 + a1 * z + a0 = &0 <=> (w pow 3) pow 2 - q * (w pow 3) - p pow 3 / &27 = &0)`;; ...
# REAL_RING `s pow 2 = &2 ==> (x pow 4 + &1 = &0 <=> x pow 2 + s * x + &1 = &0 \/ x pow 2 - s * x + &1 = &0)`;; ...
# REAL_RING `x pow 4 + 1 = &0 ==> F`;; Exception: Failure "tryfind".
# needs "Library/transc.ml";;
# g `(--((&7 * cos x pow 6) * sin x) * &7) / &49 - (--((&5 * cos x pow 4) * sin x) * &5) / &25 * &3 + --((&3 * cos x pow 2) * sin x) + sin x = sin x pow 7`;;
# SIN_CIRCLE;; val it : thm = |- !x. sin x pow 2 + cos x pow 2 = &1
# e(MP_TAC(SPEC `x:real` SIN_CIRCLE) THEN CONV_TAC REAL_RING);; 2 basis elements and 0 critical pairs val it : goalstack = No subgoals