src/HOL/MicroJava/J/TypeRel.thy
changeset 8106 de9fae0cdfde
parent 8082 381716a86fcb
child 9246 91423cd08c6f
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Jan 05 16:13:05 2000 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jan 05 18:27:07 2000 +0100
     1.3 @@ -15,13 +15,13 @@
     1.4  
     1.5  syntax
     1.6    subcls1	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
     1.7 -  subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C _"	 [71,71,71] 70)
     1.8 +  subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
     1.9    widen		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
    1.10    cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<Rightarrow>? _"[71,71,71] 70)
    1.11  
    1.12  translations
    1.13    	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
    1.14 -	"G\\<turnstile>C \\<prec>C  D" == "(C,D) \\<in> (subcls1 G)^*"
    1.15 +	"G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
    1.16  	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    1.17  	"G\\<turnstile>S \\<Rightarrow>?  T" == "(S,T) \\<in> cast    G"
    1.18  
    1.19 @@ -66,11 +66,11 @@
    1.20  inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
    1.21  			     i.e. sort of syntactic subtyping *)
    1.22    refl	              "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
    1.23 -  subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
    1.24 +  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
    1.25    null	              "G\\<turnstile>     NT \\<preceq> RefT R"
    1.26  
    1.27  inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *)
    1.28    widen	 "G\\<turnstile>S\\<preceq>T  \\<Longrightarrow> G\\<turnstile>      S \\<Rightarrow>? T"
    1.29 -  subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
    1.30 +  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
    1.31  
    1.32  end