changeset 70009 | 435fb018e8ee |
parent 67399 | eab6ce8368fa |
child 80768 | c7723cc15de8 |
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Thu Mar 28 21:22:44 2019 +0100 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Thu Mar 28 21:24:55 2019 +0100 @@ -113,7 +113,8 @@ text \<open>We can export code:\<close> -export_code fnil fcons fappend fmap ffilter fset fmember in SML +export_code fnil fcons fappend fmap ffilter fset fmember in SML file_prefix fset + subsection \<open>Using transfer with type \<open>fset\<close>\<close>