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 \\ [cname, cname] \\ bool" ("_\\_\\C1_" [71,71,71] 70) subcls :: "'c prog \\ [cname, cname] \\ bool" ("_\\_\\C _" [71,71,71] 70) widen :: "'c prog \\ [ty, ty] \\ bool" ("_\\_\\_" [71,71,71] 70) - cast :: "'c prog \\ [ty, ty] \\ bool" ("_\\_\\? _"[71,71,71] 70) + cast :: "'c prog \\ [ty, ty] \\ bool" ("_\\_\\? _"[71,71,71] 70) translations "G\\C \\C1 D" == "(C,D) \\ subcls1 G" "G\\C \\C D" == "(C,D) \\ (subcls1 G)^*" "G\\S \\ T" == "(S,T) \\ widen G" - "G\\S \\? T" == "(S,T) \\ cast G" + "G\\S \\? T" == "(S,T) \\ cast G" defs @@ -69,8 +69,8 @@ subcls "G\\C\\C D \\ G\\Class C \\ Class D" null "G\\ NT \\ RefT R" -inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *) - widen "G\\S\\T \\ G\\ S \\? T" - subcls "G\\C\\C D \\ G\\Class D \\? Class C" +inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *) + widen "G\\S\\T \\ G\\ S \\? T" + subcls "G\\C\\C D \\ G\\Class D \\? Class C" end