src/HOL/MicroJava/J/Decl.thy
changeset 42463 f270e3e18be5
parent 35431 8758fe1fc9f8
child 58886 8a6cac7c7247
     1.1 --- a/src/HOL/MicroJava/J/Decl.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/J/Decl.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -7,18 +7,23 @@
     1.4  
     1.5  theory Decl imports Type begin
     1.6  
     1.7 -types 
     1.8 +type_synonym 
     1.9    fdecl    = "vname \<times> ty"        -- "field declaration, cf. 8.3 (, 9.3)"
    1.10  
    1.11 +type_synonym
    1.12    sig      = "mname \<times> ty list"   -- "signature of a method, cf. 8.4.2"
    1.13  
    1.14 +type_synonym
    1.15    'c mdecl = "sig \<times> ty \<times> 'c"     -- "method declaration in a class"
    1.16  
    1.17 +type_synonym
    1.18    'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list" 
    1.19    -- "class = superclass, fields, methods"
    1.20  
    1.21 +type_synonym
    1.22    'c cdecl = "cname \<times> 'c class"  -- "class declaration, cf. 8.1"
    1.23  
    1.24 +type_synonym
    1.25    'c prog  = "'c cdecl list"     -- "program"
    1.26  
    1.27