equal
deleted
inserted
replaced
1214 |
1214 |
1215 Goal "exp u = x ==> ln x = u"; |
1215 Goal "exp u = x ==> ln x = u"; |
1216 by Auto_tac; |
1216 by Auto_tac; |
1217 qed "exp_ln_eq"; |
1217 qed "exp_ln_eq"; |
1218 |
1218 |
1219 Addsimps [hypreal_less_not_refl]; |
|
1220 |
1219 |
1221 (* ------------------------------------------------------------------------ *) |
1220 (* ------------------------------------------------------------------------ *) |
1222 (* Basic properties of the trig functions *) |
1221 (* Basic properties of the trig functions *) |
1223 (* ------------------------------------------------------------------------ *) |
1222 (* ------------------------------------------------------------------------ *) |
1224 |
1223 |