Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/J/TypeRel.thy
changeset 8082 381716a86fcb
parent 8034 6fc37b5c5e98
child 8106 de9fae0cdfde 
--- a/src/HOL/MicroJava/J/TypeRel.thy	Thu Dec 23 19:59:50 1999 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon Jan 03 14:07:08 2000 +0100
@@ -21,7 +21,7 @@
 
 translations
   	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
-	"G\\<turnstile>C \\<prec>C  D" == "(C,D) \\<in> (subcls1 G)^+"
+	"G\\<turnstile>C \\<prec>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"
isabelle