src/HOL/Groups.thy
changeset 61605 1bf7b186542e
parent 61378 3e04c9ca001a
child 61762 d50b993b4fb9
     1.1 --- a/src/HOL/Groups.thy	Mon Nov 09 13:49:56 2015 +0100
     1.2 +++ b/src/HOL/Groups.thy	Mon Nov 09 15:48:17 2015 +0100
     1.3 @@ -131,7 +131,7 @@
     1.4    assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
     1.5  begin
     1.6  
     1.7 -sublocale add!: semigroup plus
     1.8 +sublocale add: semigroup plus
     1.9    by standard (fact add_assoc)
    1.10  
    1.11  end
    1.12 @@ -142,7 +142,7 @@
    1.13    assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
    1.14  begin
    1.15  
    1.16 -sublocale add!: abel_semigroup plus
    1.17 +sublocale add: abel_semigroup plus
    1.18    by standard (fact add_commute)
    1.19  
    1.20  declare add.left_commute [algebra_simps, field_simps]
    1.21 @@ -159,7 +159,7 @@
    1.22    assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
    1.23  begin
    1.24  
    1.25 -sublocale mult!: semigroup times
    1.26 +sublocale mult: semigroup times
    1.27    by standard (fact mult_assoc)
    1.28  
    1.29  end
    1.30 @@ -170,7 +170,7 @@
    1.31    assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
    1.32  begin
    1.33  
    1.34 -sublocale mult!: abel_semigroup times
    1.35 +sublocale mult: abel_semigroup times
    1.36    by standard (fact mult_commute)
    1.37  
    1.38  declare mult.left_commute [algebra_simps, field_simps]
    1.39 @@ -188,7 +188,7 @@
    1.40      and add_0_right: "a + 0 = a"
    1.41  begin
    1.42  
    1.43 -sublocale add!: monoid plus 0
    1.44 +sublocale add: monoid plus 0
    1.45    by standard (fact add_0_left add_0_right)+
    1.46  
    1.47  end
    1.48 @@ -203,7 +203,7 @@
    1.49  subclass monoid_add
    1.50    by standard (simp_all add: add_0 add.commute [of _ 0])
    1.51  
    1.52 -sublocale add!: comm_monoid plus 0
    1.53 +sublocale add: comm_monoid plus 0
    1.54    by standard (simp add: ac_simps)
    1.55  
    1.56  end
    1.57 @@ -213,7 +213,7 @@
    1.58      and mult_1_right: "a * 1 = a"
    1.59  begin
    1.60  
    1.61 -sublocale mult!: monoid times 1
    1.62 +sublocale mult: monoid times 1
    1.63    by standard (fact mult_1_left mult_1_right)+
    1.64  
    1.65  end
    1.66 @@ -228,7 +228,7 @@
    1.67  subclass monoid_mult
    1.68    by standard (simp_all add: mult_1 mult.commute [of _ 1])
    1.69  
    1.70 -sublocale mult!: comm_monoid times 1
    1.71 +sublocale mult: comm_monoid times 1
    1.72    by standard (simp add: ac_simps)
    1.73  
    1.74  end