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/WellForm.thy
changeset 8034 6fc37b5c5e98
parent 8011 d14c4e9e9c8e
child 8082 381716a86fcb 
--- a/src/HOL/MicroJava/J/WellForm.thy	Thu Nov 25 12:30:57 1999 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Fri Nov 26 08:46:59 1999 +0100
@@ -38,7 +38,7 @@
          | Some D \\<Rightarrow>
              is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<prec>C C \\<and>
              (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
-                 cmethd(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
+                 method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
 
  wf_prog	:: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> bool"
 "wf_prog wtm G \\<equiv>
isabelle