src/HOL/MicroJava/J/Decl.thy
changeset 10042 7164dc0d24d8
parent 9346 297dcbf64526
child 10613 78b1d6c3ee9c
     1.1 --- a/src/HOL/MicroJava/J/Decl.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Decl.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -32,26 +32,26 @@
     1.4  
     1.5  defs 
     1.6  
     1.7 - ObjectC_def "ObjectC \\<equiv> (Object, (None, [], []))"
     1.8 + ObjectC_def "ObjectC == (Object, (None, [], []))"
     1.9  
    1.10  
    1.11  types 'c prog = "'c cdecl list"
    1.12  
    1.13  consts
    1.14  
    1.15 -  class		:: "'c prog \\<Rightarrow> (cname \\<leadsto> 'c class)"
    1.16 +  class		:: "'c prog => (cname \\<leadsto> 'c class)"
    1.17  
    1.18 -  is_class	:: "'c prog \\<Rightarrow> cname \\<Rightarrow> bool"
    1.19 -  is_type	:: "'c prog \\<Rightarrow> ty    \\<Rightarrow> bool"
    1.20 +  is_class	:: "'c prog => cname => bool"
    1.21 +  is_type	:: "'c prog => ty    => bool"
    1.22  
    1.23  defs
    1.24  
    1.25 -  class_def	"class        \\<equiv> map_of"
    1.26 +  class_def	"class        == map_of"
    1.27  
    1.28 -  is_class_def	"is_class G C \\<equiv> class G C \\<noteq> None"
    1.29 +  is_class_def	"is_class G C == class G C \\<noteq> None"
    1.30  
    1.31  primrec
    1.32  "is_type G (PrimT pt) = True"
    1.33 -"is_type G (RefT t) = (case t of NullT \\<Rightarrow> True | ClassT C \\<Rightarrow> is_class G C)"
    1.34 +"is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
    1.35  
    1.36  end