src/HOL/MicroJava/J/TypeRel.thy
changeset 9246 91423cd08c6f
parent 8106 de9fae0cdfde
child 9346 297dcbf64526
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Jul 04 15:58:11 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jul 05 10:28:29 2000 +0200
     1.3 @@ -17,13 +17,13 @@
     1.4    subcls1	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
     1.5    subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
     1.6    widen		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
     1.7 -  cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<Rightarrow>? _"[71,71,71] 70)
     1.8 +  cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
     1.9  
    1.10  translations
    1.11    	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
    1.12  	"G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
    1.13  	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    1.14 -	"G\\<turnstile>S \\<Rightarrow>?  T" == "(S,T) \\<in> cast    G"
    1.15 +	"G\\<turnstile>S \\<preceq>?  T" == "(S,T) \\<in> cast    G"
    1.16  
    1.17  defs
    1.18  
    1.19 @@ -69,8 +69,8 @@
    1.20    subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
    1.21    null	              "G\\<turnstile>     NT \\<preceq> RefT R"
    1.22  
    1.23 -inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *)
    1.24 -  widen	 "G\\<turnstile>S\\<preceq>T  \\<Longrightarrow> G\\<turnstile>      S \\<Rightarrow>? T"
    1.25 -  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
    1.26 +inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
    1.27 +  widen	 "G\\<turnstile>S\\<preceq>T   \\<Longrightarrow> G\\<turnstile>      S \\<preceq>? T"
    1.28 +  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<preceq>? Class C"
    1.29  
    1.30  end