changeset 61560 | 7c985fd653c5 |
parent 61524 | f2e51e704a96 |
child 61610 | 4f54d2759a0b |
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Nov 03 16:35:38 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Nov 03 16:47:37 2015 +0100 @@ -5,7 +5,7 @@ section \<open>Complex Transcendental Functions\<close> theory Complex_Transcendental -imports "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics" +imports Complex_Analysis_Basics begin lemma cmod_add_real_less: