changeset 49834 | b27bbb021df1 |
parent 48757 | 1232760e208e |
child 49962 | a8cc904a6820 |
--- a/src/HOL/Library/Formal_Power_Series.thy Fri Oct 12 15:08:29 2012 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Fri Oct 12 18:58:20 2012 +0200 @@ -11,7 +11,7 @@ subsection {* The type of formal power series*} -typedef (open) 'a fps = "{f :: nat \<Rightarrow> 'a. True}" +typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}" morphisms fps_nth Abs_fps by simp