src/HOL/MicroJava/J/WellForm.thy
changeset 42463 f270e3e18be5
parent 35416 d8d7d1b785af
child 42793 88bee9f6eec7
     1.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  \end{itemize}
     1.5  \end{description}
     1.6  *}
     1.7 -types 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
     1.8 +type_synonym 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
     1.9  
    1.10  definition wf_syscls :: "'c prog => bool" where
    1.11  "wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)"