# HG changeset patch
# User oheimb
# Date 962785709 -7200
# Node ID 91423cd08c6f553ffae6ffc1b4974245c1d73a89
# Parent  428385c4bc50801ad696fa844649ba58616a781a
corrected symbol for casting relation

diff -r 428385c4bc50 -r 91423cd08c6f src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Tue Jul 04 15:58:11 2000 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Jul 05 10:28:29 2000 +0200
@@ -30,7 +30,7 @@
 qed "NewC_conforms";
 
 Goalw [cast_ok_def]
- "\\<lbrakk> wf_prog wf_mb G; G,h\\<turnstile>v\\<Colon>\\<preceq>Tb; G\\<turnstile>Tb\\<Rightarrow>? T'; cast_ok G T' h v\\<rbrakk> \
+ "\\<lbrakk> wf_prog wf_mb G; G,h\\<turnstile>v\\<Colon>\\<preceq>Tb; G\\<turnstile>Tb\\<preceq>? T'; cast_ok G T' h v\\<rbrakk> \
 \ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
 by( case_tac1 "v = Null" 1);
 by(  Asm_full_simp_tac 1);
diff -r 428385c4bc50 -r 91423cd08c6f src/HOL/MicroJava/J/TypeRel.ML
--- a/src/HOL/MicroJava/J/TypeRel.ML	Tue Jul 04 15:58:11 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.ML	Wed Jul 05 10:28:29 2000 +0200
@@ -117,14 +117,14 @@
 
 val prove_cast_lemma = prove_typerel_lemma [] cast.elim;
 
-val cast_RefT = prove_typerel "G\\<turnstile>RefT R\\<Rightarrow>? T \\<Longrightarrow> \\<exists>t. T=RefT t" 
+val cast_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>? T \\<Longrightarrow> \\<exists>t. T=RefT t" 
 	[prove_typerel_lemma [widen_RefT] cast.elim 
-	"G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
+	"G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
 
-val cast_RefT2 = prove_typerel "G\\<turnstile>S\\<Rightarrow>? RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" 
+val cast_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>? RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" 
 	[prove_typerel_lemma [widen_RefT2] cast.elim 
-	"G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
+	"G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
 
-val cast_PrimT2 = prove_typerel "G\\<turnstile>S\\<Rightarrow>? PrimT pt \\<Longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt" 
- [prove_cast_lemma "G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> T=PrimT pt \\<longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt"];
+val cast_PrimT2 = prove_typerel "G\\<turnstile>S\\<preceq>? PrimT pt \\<Longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt" 
+ [prove_cast_lemma "G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> T=PrimT pt \\<longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt"];
 
diff -r 428385c4bc50 -r 91423cd08c6f src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Jul 04 15:58:11 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jul 05 10:28:29 2000 +0200
@@ -17,13 +17,13 @@
   subcls1	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
   subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
   widen		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
-  cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<Rightarrow>? _"[71,71,71] 70)
+  cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
 
 translations
   	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
 	"G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
 	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
-	"G\\<turnstile>S \\<Rightarrow>?  T" == "(S,T) \\<in> cast    G"
+	"G\\<turnstile>S \\<preceq>?  T" == "(S,T) \\<in> cast    G"
 
 defs
 
@@ -69,8 +69,8 @@
   subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
   null	              "G\\<turnstile>     NT \\<preceq> RefT R"
 
-inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *)
-  widen	 "G\\<turnstile>S\\<preceq>T  \\<Longrightarrow> G\\<turnstile>      S \\<Rightarrow>? T"
-  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
+inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
+  widen	 "G\\<turnstile>S\\<preceq>T   \\<Longrightarrow> G\\<turnstile>      S \\<preceq>? T"
+  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<preceq>? Class C"
 
 end
diff -r 428385c4bc50 -r 91423cd08c6f src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Tue Jul 04 15:58:11 2000 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy	Wed Jul 05 10:28:29 2000 +0200
@@ -96,7 +96,7 @@
 
   (* cf. 15.15 *)
   Cast	"\\<lbrakk>E\\<turnstile>e\\<Colon>T;
-	  prg E\\<turnstile>T\\<Rightarrow>? T'\\<rbrakk> \\<Longrightarrow>
+	  prg E\\<turnstile>T\\<preceq>? T'\\<rbrakk> \\<Longrightarrow>
 						 E\\<turnstile>Cast T' e\\<Colon>T'"
 
   (* cf. 15.7.1 *)