src/HOL/NanoJava/Decl.thy
changeset 42463 f270e3e18be5
parent 35431 8758fe1fc9f8
child 44375 dfc2e722fe47
     1.1 --- a/src/HOL/NanoJava/Decl.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/NanoJava/Decl.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    | Class cname  --{* class type *}
     1.5  
     1.6  text{* Field declaration *}
     1.7 -types   fdecl           
     1.8 +type_synonym fdecl           
     1.9          = "fname \<times> ty"
    1.10  
    1.11  record  methd           
    1.12 @@ -22,7 +22,7 @@
    1.13            bdy :: stmt
    1.14  
    1.15  text{* Method declaration *}
    1.16 -types   mdecl
    1.17 +type_synonym mdecl
    1.18          = "mname \<times> methd"
    1.19  
    1.20  record  "class"
    1.21 @@ -31,10 +31,10 @@
    1.22            methods ::"mdecl list"
    1.23  
    1.24  text{* Class declaration *}
    1.25 -types   cdecl
    1.26 +type_synonym cdecl
    1.27          = "cname \<times> class"
    1.28  
    1.29 -types   prog
    1.30 +type_synonym prog
    1.31          = "cdecl list"
    1.32  
    1.33  translations