--- a/src/HOL/MicroJava/J/Conform.thy Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Fri Jul 14 16:32:51 2000 +0200
@@ -6,7 +6,9 @@
Conformity relations for type safety of Java
*)
-Conform = State +
+Conform = State + WellType +
+
+types 'c env_ = "'c prog \\<times> (vname \\<leadsto> ty)" (* same as env of WellType.thy *)
constdefs
@@ -26,7 +28,7 @@
hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool" ("_\\<turnstile>h _\\<surd>" [51,51] 50)
"G\\<turnstile>h h\\<surd> \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
- conforms :: "state \\<Rightarrow> java_mb env \\<Rightarrow> bool" ("_\\<Colon>\\<preceq>_" [51,51] 50)
+ conforms :: "state \\<Rightarrow> java_mb env_ \\<Rightarrow> bool" ("_\\<Colon>\\<preceq>_" [51,51] 50)
"s\\<Colon>\\<preceq>E \\<equiv> prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
end