changeset 65380 | ae93953746fc |
parent 62175 | 8ffc4d0e652d |
child 67312 | 0d25e02759b7 |
--- a/src/HOL/HOLCF/Map_Functions.thy Tue Apr 04 21:45:54 2017 +0200 +++ b/src/HOL/HOLCF/Map_Functions.thy Tue Apr 04 21:57:43 2017 +0200 @@ -5,7 +5,7 @@ section \<open>Map functions for various types\<close> theory Map_Functions -imports Deflation +imports Deflation Sprod Ssum Sfun Up begin subsection \<open>Map operator for continuous function space\<close>