changeset 41413 | 64cd30d6b0b8 |
parent 41096 | 843c40bbc379 |
child 41544 | c3b977fee8a3 |
--- a/src/HOL/Probability/Positive_Extended_Real.thy Wed Dec 29 13:51:17 2010 +0100 +++ b/src/HOL/Probability/Positive_Extended_Real.thy Wed Dec 29 17:34:41 2010 +0100 @@ -3,7 +3,7 @@ header {* A type for positive real numbers with infinity *} theory Positive_Extended_Real - imports Complex_Main Nat_Bijection Multivariate_Analysis + imports Complex_Main "~~/src/HOL/Library/Nat_Bijection" Multivariate_Analysis begin lemma (in complete_lattice) Sup_start: