changeset 48891 | c0eafbd55de3 |
parent 47937 | 70375fa2679d |
child 49975 | faf4afed009f |
--- a/src/HOL/Transfer.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Transfer.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,7 +6,6 @@ theory Transfer imports Plain Hilbert_Choice -uses ("Tools/transfer.ML") begin subsection {* Relator for function space *} @@ -96,8 +95,7 @@ shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)" using assms unfolding Rel_def fun_rel_def by fast -use "Tools/transfer.ML" - +ML_file "Tools/transfer.ML" setup Transfer.setup declare fun_rel_eq [relator_eq]