# HG changeset patch
# User haftmann
# Date 1179567203 -7200
# Node ID 019d44d4683483fd00a51478c8cc44e7d4058b5f
# Parent  1d29bc31b0cb6c98f67ebc01df5b80f0d62ba6b4
hide locale predicate "field" from HOL library

diff -r 1d29bc31b0cb -r 019d44d46834 src/HOL/Bali/TypeSafe.thy
--- 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"