--- a/src/HOL/Bali/TypeSafe.thy Sat May 19 11:33:22 2007 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Sat May 19 11:33:23 2007 +0200
@@ -4,10 +4,14 @@
*)
header {* The type soundness proof for Java *}
-theory TypeSafe imports DefiniteAssignmentCorrect Conform begin
+theory TypeSafe
+imports DefiniteAssignmentCorrect Conform
+begin
section "error free"
+hide const field
+
lemma error_free_halloc:
assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
error_free_s0: "error_free s0"