src/HOL/Library/Numeral_Type.thy
changeset 36350 bc7982c54e37
parent 35431 8758fe1fc9f8
child 37653 847e95ca9b0a
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Mon Apr 26 11:34:17 2010 +0200
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Apr 26 11:34:19 2010 +0200
     1.3 @@ -213,7 +213,7 @@
     1.4  
     1.5  lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
     1.6  apply (intro_classes, unfold definitions)
     1.7 -apply (simp_all add: Rep_simps zmod_simps ring_simps)
     1.8 +apply (simp_all add: Rep_simps zmod_simps field_simps)
     1.9  done
    1.10  
    1.11  end