Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid ambiguity of State.state vs. JVMType.state;
authorwenzelm
Thu, 27 Mar 2008 21:21:08 +0100
changeset 26453 758c6fef7b94
parent 26452 ed657432b8b9
child 26454 57923fdab83b
avoid ambiguity of State.state vs. JVMType.state;
src/HOL/MicroJava/BV/BVSpec.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Thu Mar 27 19:49:24 2008 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Mar 27 21:21:08 2008 +0100
@@ -23,7 +23,7 @@
                      (\<forall>e \<in> set et. fst (snd (snd e)) < length ins)"
 
   -- "The method type only contains declared classes:"
-  check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state list \<Rightarrow> bool"
+  check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool"
   "check_types G mxs mxr phi \<equiv> set phi \<subseteq> states G mxs mxr"
 
   -- "An instruction is welltyped if it is applicable and its effect"
isabelle