src/HOL/Number_Theory/MiscAlgebra.thy
changeset 35416 d8d7d1b785af
parent 32479 521cc9bf2958
child 41541 1fa4725c4656
     1.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -31,8 +31,7 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -constdefs 
     1.8 -  units_of :: "('a, 'b) monoid_scheme => 'a monoid"
     1.9 +definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
    1.10    "units_of G == (| carrier = Units G,
    1.11       Group.monoid.mult = Group.monoid.mult G,
    1.12       one  = one G |)";