src/HOL/Groups_List.thy
changeset 61605 1bf7b186542e
parent 61566 c3d6e570ccef
child 61776 57bb7da5c867
     1.1 --- a/src/HOL/Groups_List.thy	Mon Nov 09 13:49:56 2015 +0100
     1.2 +++ b/src/HOL/Groups_List.thy	Mon Nov 09 15:48:17 2015 +0100
     1.3 @@ -65,12 +65,12 @@
     1.4  where
     1.5    "listsum  = monoid_list.F plus 0"
     1.6  
     1.7 -sublocale listsum!: monoid_list plus 0
     1.8 +sublocale listsum: monoid_list plus 0
     1.9  rewrites
    1.10   "monoid_list.F plus 0 = listsum"
    1.11  proof -
    1.12    show "monoid_list plus 0" ..
    1.13 -  then interpret listsum!: monoid_list plus 0 .
    1.14 +  then interpret listsum: monoid_list plus 0 .
    1.15    from listsum_def show "monoid_list.F plus 0 = listsum" by rule
    1.16  qed
    1.17   
    1.18 @@ -79,22 +79,22 @@
    1.19  context comm_monoid_add
    1.20  begin
    1.21  
    1.22 -sublocale listsum!: comm_monoid_list plus 0
    1.23 +sublocale listsum: comm_monoid_list plus 0
    1.24  rewrites
    1.25    "monoid_list.F plus 0 = listsum"
    1.26  proof -
    1.27    show "comm_monoid_list plus 0" ..
    1.28 -  then interpret listsum!: comm_monoid_list plus 0 .
    1.29 +  then interpret listsum: comm_monoid_list plus 0 .
    1.30    from listsum_def show "monoid_list.F plus 0 = listsum" by rule
    1.31  qed
    1.32  
    1.33 -sublocale setsum!: comm_monoid_list_set plus 0
    1.34 +sublocale setsum: comm_monoid_list_set plus 0
    1.35  rewrites
    1.36    "monoid_list.F plus 0 = listsum"
    1.37    and "comm_monoid_set.F plus 0 = setsum"
    1.38  proof -
    1.39    show "comm_monoid_list_set plus 0" ..
    1.40 -  then interpret setsum!: comm_monoid_list_set plus 0 .
    1.41 +  then interpret setsum: comm_monoid_list_set plus 0 .
    1.42    from listsum_def show "monoid_list.F plus 0 = listsum" by rule
    1.43    from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
    1.44  qed
    1.45 @@ -332,12 +332,12 @@
    1.46  where
    1.47    "listprod  = monoid_list.F times 1"
    1.48  
    1.49 -sublocale listprod!: monoid_list times 1
    1.50 +sublocale listprod: monoid_list times 1
    1.51  rewrites
    1.52    "monoid_list.F times 1 = listprod"
    1.53  proof -
    1.54    show "monoid_list times 1" ..
    1.55 -  then interpret listprod!: monoid_list times 1 .
    1.56 +  then interpret listprod: monoid_list times 1 .
    1.57    from listprod_def show "monoid_list.F times 1 = listprod" by rule
    1.58  qed
    1.59  
    1.60 @@ -346,22 +346,22 @@
    1.61  context comm_monoid_mult
    1.62  begin
    1.63  
    1.64 -sublocale listprod!: comm_monoid_list times 1
    1.65 +sublocale listprod: comm_monoid_list times 1
    1.66  rewrites
    1.67    "monoid_list.F times 1 = listprod"
    1.68  proof -
    1.69    show "comm_monoid_list times 1" ..
    1.70 -  then interpret listprod!: comm_monoid_list times 1 .
    1.71 +  then interpret listprod: comm_monoid_list times 1 .
    1.72    from listprod_def show "monoid_list.F times 1 = listprod" by rule
    1.73  qed
    1.74  
    1.75 -sublocale setprod!: comm_monoid_list_set times 1
    1.76 +sublocale setprod: comm_monoid_list_set times 1
    1.77  rewrites
    1.78    "monoid_list.F times 1 = listprod"
    1.79    and "comm_monoid_set.F times 1 = setprod"
    1.80  proof -
    1.81    show "comm_monoid_list_set times 1" ..
    1.82 -  then interpret setprod!: comm_monoid_list_set times 1 .
    1.83 +  then interpret setprod: comm_monoid_list_set times 1 .
    1.84    from listprod_def show "monoid_list.F times 1 = listprod" by rule
    1.85    from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
    1.86  qed