deriv_trig : THEORY BEGIN trigl: LIBRARY = "../trig" IMPORTING derivatives_con[real], trigl@trig diff_sin : AXIOM derivable(sin) diff_sin_jdg : JUDGEMENT sin HAS_TYPE deriv_fun deriv_sin : AXIOM deriv(sin) = cos diff_cos : AXIOM derivable(cos) diff_cos_jdg : JUDGEMENT cos HAS_TYPE deriv_fun deriv_cos : AXIOM deriv(cos) = LAMBDA(t:real):-sin(t) END deriv_trig