src/HOL/Bali/WellType.thy
changeset 33965 f57c11db4ad4
parent 32960 69916a850301
child 35067 af4c18c30593
     1.1 --- a/src/HOL/Bali/WellType.thy	Fri Nov 27 08:42:34 2009 +0100
     1.2 +++ b/src/HOL/Bali/WellType.thy	Fri Nov 27 08:42:50 2009 +0100
     1.3 @@ -1,10 +1,11 @@
     1.4  (*  Title:      HOL/Bali/WellType.thy
     1.5 -    ID:         $Id$
     1.6      Author:     David von Oheimb
     1.7  *)
     1.8  header {* Well-typedness of Java programs *}
     1.9  
    1.10 -theory WellType imports DeclConcepts begin
    1.11 +theory WellType
    1.12 +imports DeclConcepts
    1.13 +begin
    1.14  
    1.15  text {*
    1.16  improvements over Java Specification 1.0:
    1.17 @@ -443,10 +444,10 @@
    1.18  
    1.19  translations
    1.20          "E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
    1.21 -        "E\<turnstile>s\<Colon>\<surd>"  == "E\<turnstile>In1r s\<Colon>Inl (PrimT Void)"
    1.22 -        "E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>Inl T"
    1.23 -        "E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2  e\<Colon>Inl T"
    1.24 -        "E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>Inr T"
    1.25 +        "E\<turnstile>s\<Colon>\<surd>"  == "E\<turnstile>In1r s\<Colon>CONST Inl (PrimT Void)"
    1.26 +        "E\<turnstile>e\<Colon>-T" == "E\<turnstile>In1l e\<Colon>CONST Inl T"
    1.27 +        "E\<turnstile>e\<Colon>=T" == "E\<turnstile>In2  e\<Colon>CONST Inl T"
    1.28 +        "E\<turnstile>e\<Colon>\<doteq>T" == "E\<turnstile>In3  e\<Colon>CONST Inr T"
    1.29  
    1.30  
    1.31  declare not_None_eq [simp del]