| changeset 13601 | fd3e3d6b37b2 |
| parent 13097 | c9c7f23d0ceb |
| child 13958 | c1c67582c9b5 |
--- a/src/HOL/Hyperreal/Transcendental.ML Mon Sep 30 16:12:16 2002 +0200 +++ b/src/HOL/Hyperreal/Transcendental.ML Mon Sep 30 16:14:02 2002 +0200 @@ -1132,7 +1132,7 @@ qed "ln_mult"; Goal "[| 0 < x; 0 < y |] ==> (ln x = ln y) = (x = y)"; -by (auto_tac (claset() addSDs [(exp_ln_iff RS iffD2)],simpset())); +by (auto_tac (claset() addSDs [(exp_ln_iff RS iffD2 RS sym)],simpset())); qed "ln_inj_iff"; Addsimps [ln_inj_iff];