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 28562 4e74209f113e
parent 28524 644b62cf678f
child 32461 eee4fa79398f 
--- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -68,7 +68,7 @@
 definition
   "wf_class G = wfP ((subcls1 G)^--1)"
 
-lemma class_rec_func (*[code func]*):
+lemma class_rec_func (*[code]*):
   "class_rec G C t f = (if wf_class G then
     (case class G C
       of None \<Rightarrow> undefined
isabelle