src/HOL/Bali/DeclConcepts.thy
changeset 37678 0040bafffdef
parent 37406 982f3e02f3c4
child 37956 ee939247b2fb
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Thu Jul 01 16:54:44 2010 +0200
     1.3 @@ -109,7 +109,7 @@
     1.4  lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
     1.5  by (simp add: decl_acc_modi_def)
     1.6  
     1.7 -instantiation * :: (type, has_accmodi) has_accmodi
     1.8 +instantiation prod :: (type, has_accmodi) has_accmodi
     1.9  begin
    1.10  
    1.11  definition
    1.12 @@ -165,7 +165,7 @@
    1.13  lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
    1.14  by (simp add: qtname_declclass_def)
    1.15  
    1.16 -instantiation * :: (has_declclass, type) has_declclass
    1.17 +instantiation prod :: (has_declclass, type) has_declclass
    1.18  begin
    1.19  
    1.20  definition
    1.21 @@ -204,7 +204,7 @@
    1.22  lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
    1.23  by (simp add: static_field_type_is_static_def)
    1.24  
    1.25 -instantiation * :: (type, has_static) has_static
    1.26 +instantiation prod :: (type, has_static) has_static
    1.27  begin
    1.28  
    1.29  definition
    1.30 @@ -472,7 +472,7 @@
    1.31  lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
    1.32  by (simp add: mhead_def mhead_resTy_simp)
    1.33  
    1.34 -instantiation * :: ("type","has_resTy") has_resTy
    1.35 +instantiation prod :: ("type","has_resTy") has_resTy
    1.36  begin
    1.37  
    1.38  definition