changeset 51112 | da97167e03f7 |
parent 49975 | faf4afed009f |
child 51437 | 8739f8abbecb |
--- a/src/HOL/Transfer.thy Thu Feb 14 13:16:47 2013 +0100 +++ b/src/HOL/Transfer.thy Thu Feb 14 12:24:42 2013 +0100 @@ -5,7 +5,7 @@ header {* Generic theorem transfer using relations *} theory Transfer -imports Plain Hilbert_Choice +imports Hilbert_Choice begin subsection {* Relator for function space *}