src/HOL/Transfer.thy
changeset 55811 aa1acc25126b
parent 55760 aaaccc8e015f
child 55945 e96383acecf9
     1.1 --- a/src/HOL/Transfer.thy	Fri Feb 28 22:00:13 2014 +0100
     1.2 +++ b/src/HOL/Transfer.thy	Fri Feb 28 17:54:52 2014 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Generic theorem transfer using relations *}
     1.5  
     1.6  theory Transfer
     1.7 -imports Hilbert_Choice Basic_BNFs
     1.8 +imports Hilbert_Choice Basic_BNFs Metis
     1.9  begin
    1.10  
    1.11  subsection {* Relator for function space *}