src/HOL/MicroJava/J/TypeRel.thy
changeset 8082 381716a86fcb
parent 8034 6fc37b5c5e98
child 8106 de9fae0cdfde
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Thu Dec 23 19:59:50 1999 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon Jan 03 14:07:08 2000 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4  
     1.5  translations
     1.6    	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
     1.7 -	"G\\<turnstile>C \\<prec>C  D" == "(C,D) \\<in> (subcls1 G)^+"
     1.8 +	"G\\<turnstile>C \\<prec>C  D" == "(C,D) \\<in> (subcls1 G)^*"
     1.9  	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    1.10  	"G\\<turnstile>S \\<Rightarrow>?  T" == "(S,T) \\<in> cast    G"
    1.11