src/HOL/MicroJava/J/TypeRel.thy
changeset 10061 fe82134773dc
parent 10042 7164dc0d24d8
child 10138 412a3ced6efd
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Sep 22 16:28:04 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Sep 22 16:28:53 2000 +0200
     1.3 @@ -9,21 +9,27 @@
     1.4  TypeRel = Decl +
     1.5  
     1.6  consts
     1.7 -  subcls1	:: "'c prog => (cname \\<times> cname) set"  (* subclass *)
     1.8 -  widen 	:: "'c prog => (ty    \\<times> ty   ) set"  (* widening *)
     1.9 -  cast		:: "'c prog => (cname \\<times> cname) set"  (* casting *)
    1.10 +  subcls1 :: "'c prog => (cname \\<times> cname) set"  (* subclass *)
    1.11 +  widen   :: "'c prog => (ty    \\<times> ty   ) set"  (* widening *)
    1.12 +  cast    :: "'c prog => (cname \\<times> cname) set"  (* casting *)
    1.13  
    1.14  syntax
    1.15 -  subcls1	:: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
    1.16 -  subcls	:: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
    1.17 -  widen		:: "'c prog => [ty   , ty   ] => bool" ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
    1.18 -  cast		:: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
    1.19 +  subcls1 :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<prec>C1 _" [71,71,71] 70)
    1.20 +  subcls  :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>C _" [71,71,71] 70)
    1.21 +  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \\<turnstile> _ \\<preceq> _" [71,71,71] 70)
    1.22 +  cast    :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>? _" [71,71,71] 70)
    1.23 +
    1.24 +syntax (HTML)
    1.25 +  subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
    1.26 +  subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
    1.27 +  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _" [71,71,71] 70)
    1.28 +  cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
    1.29  
    1.30  translations
    1.31 -  	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
    1.32 -	"G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
    1.33 -	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    1.34 -	"G\\<turnstile>C \\<preceq>?  D" == "(C,D) \\<in> cast    G"
    1.35 +  "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
    1.36 +  "G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
    1.37 +  "G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    1.38 +  "G\\<turnstile>C \\<preceq>?  D" == "(C,D) \\<in> cast    G"
    1.39  
    1.40  defs
    1.41