changeset 46868 | 6c250adbe101 |
parent 46236 | ae79f2978a67 |
child 47108 | 2a1953f0d20d |
--- a/src/HOL/Library/Numeral_Type.thy Sun Mar 11 13:39:16 2012 +0100 +++ b/src/HOL/Library/Numeral_Type.thy Sun Mar 11 13:54:08 2012 +0100 @@ -135,8 +135,8 @@ end -locale mod_ring = mod_type + - constrains n :: int +locale mod_ring = mod_type n Rep Abs + for n :: int and Rep :: "'a::{number_ring} \<Rightarrow> int" and Abs :: "int \<Rightarrow> 'a::{number_ring}" begin