--- a/src/HOL/MicroJava/J/WellForm.thy Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Thu Sep 21 10:42:49 2000 +0200
@@ -20,28 +20,28 @@
constdefs
- wf_fdecl :: "'c prog \\<Rightarrow> fdecl \\<Rightarrow> bool"
-"wf_fdecl G \\<equiv> \\<lambda>(fn,ft). is_type G ft"
+ wf_fdecl :: "'c prog => fdecl => bool"
+"wf_fdecl G == \\<lambda>(fn,ft). is_type G ft"
- wf_mhead :: "'c prog \\<Rightarrow> sig \\<Rightarrow> ty \\<Rightarrow> bool"
-"wf_mhead G \\<equiv> \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
+ wf_mhead :: "'c prog => sig => ty => bool"
+"wf_mhead G == \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
- wf_mdecl :: "'c wf_mb \\<Rightarrow> 'c wf_mb"
-"wf_mdecl wf_mb G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
+ wf_mdecl :: "'c wf_mb => 'c wf_mb"
+"wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
- wf_cdecl :: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
-"wf_cdecl wf_mb G \\<equiv>
+ wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
+"wf_cdecl wf_mb G ==
\\<lambda>(C,(sc,fs,ms)).
(\\<forall>f\\<in>set fs. wf_fdecl G f ) \\<and> unique fs \\<and>
(\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and> unique ms \\<and>
- (case sc of None \\<Rightarrow> C = Object
- | Some D \\<Rightarrow>
+ (case sc of None => C = Object
+ | Some D =>
is_class G D \\<and> \\<not> G\\<turnstile>D\\<preceq>C C \\<and>
(\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
- method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
+ method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
- wf_prog :: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> bool"
-"wf_prog wf_mb G \\<equiv>
+ wf_prog :: "'c wf_mb => 'c prog => bool"
+"wf_prog wf_mb G ==
let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
end