src/HOL/ex/Classpackage.thy
changeset 20597 65fe827aa595
parent 20453 855f07fabd76
child 21080 7d73aa966207
     1.1 --- a/src/HOL/ex/Classpackage.thy	Tue Sep 19 15:22:03 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Tue Sep 19 15:22:05 2006 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    from semigroup_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
     1.5  qed
     1.6  
     1.7 -instance (type) list :: semigroup
     1.8 +instance list :: (type) semigroup
     1.9    "xs \<otimes> ys \<equiv> xs @ ys"
    1.10  proof
    1.11    fix xs ys zs :: "'a list"
    1.12 @@ -52,7 +52,7 @@
    1.13    from monoidl_num_def show "\<one> \<otimes> k = k" by simp
    1.14  qed
    1.15  
    1.16 -instance (type) list :: monoidl
    1.17 +instance list :: (type) monoidl
    1.18    "\<one> \<equiv> []"
    1.19  proof
    1.20    fix xs :: "'a list"
    1.21 @@ -67,7 +67,7 @@
    1.22  class monoid = monoidl +
    1.23    assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
    1.24  
    1.25 -instance monoid_list_def: (type) list :: monoid
    1.26 +instance monoid_list_def: list :: (type) monoid
    1.27  proof
    1.28    fix xs :: "'a list"
    1.29    show "xs \<otimes> \<one> = xs"
    1.30 @@ -288,26 +288,26 @@
    1.31    "\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>"
    1.32  using pow_def nat_pow_one inv_one by simp
    1.33  
    1.34 -instance semigroup_prod_def: (semigroup, semigroup) * :: semigroup
    1.35 +instance semigroup_prod_def: * :: (semigroup, semigroup) semigroup
    1.36    mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
    1.37                (x1 \<otimes> y1, x2 \<otimes> y2)"
    1.38  by default (simp_all add: split_paired_all semigroup_prod_def assoc)
    1.39  
    1.40 -instance monoidl_prod_def: (monoidl, monoidl) * :: monoidl
    1.41 +instance monoidl_prod_def: * :: (monoidl, monoidl) monoidl
    1.42    one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
    1.43  by default (simp_all add: split_paired_all monoidl_prod_def neutl)
    1.44  
    1.45 -instance monoid_prod_def: (monoid, monoid) * :: monoid
    1.46 +instance monoid_prod_def: * :: (monoid, monoid) monoid
    1.47  by default (simp_all add: split_paired_all monoid_prod_def neutr)
    1.48  
    1.49 -instance monoid_comm_prod_def: (monoid_comm, monoid_comm) * :: monoid_comm
    1.50 +instance monoid_comm_prod_def: * :: (monoid_comm, monoid_comm) monoid_comm
    1.51  by default (simp_all add: split_paired_all monoidl_prod_def comm)
    1.52  
    1.53 -instance group_prod_def: (group, group) * :: group
    1.54 +instance group_prod_def: * :: (group, group) group
    1.55    inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
    1.56  by default (simp_all add: split_paired_all group_prod_def invl)
    1.57  
    1.58 -instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm
    1.59 +instance group_comm_prod_def: * :: (group_comm, group_comm) group_comm
    1.60  by default (simp_all add: split_paired_all group_prod_def comm)
    1.61  
    1.62  definition