src/HOL/Library/Polynomial_Factorial.thy
changeset 64911 f0e07600de47
parent 64860 4d56170d97b3
child 65366 10ca63a18e56
     1.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Tue Jan 17 11:26:21 2017 +0100
     1.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Tue Jan 17 13:59:10 2017 +0100
     1.3 @@ -52,7 +52,7 @@
     1.4  subsection \<open>Lifting elements into the field of fractions\<close>
     1.5  
     1.6  definition to_fract :: "'a :: idom \<Rightarrow> 'a fract" where "to_fract x = Fract x 1"
     1.7 -  -- \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
     1.8 +  \<comment> \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
     1.9  
    1.10  lemma to_fract_0 [simp]: "to_fract 0 = 0"
    1.11    by (simp add: to_fract_def eq_fract Zero_fract_def)