equal
deleted
inserted
replaced
96 done |
96 done |
97 |
97 |
98 |
98 |
99 |
99 |
100 |
100 |
101 (* The following def should replace the conditions in WellType.thy / wf_java_mdecl |
101 (* The following definition should replace the conditions in WellType.thy / wf_java_mdecl |
102 *) |
102 *) |
103 definition disjoint_varnames :: "[vname list, (vname \<times> ty) list] \<Rightarrow> bool" where |
103 definition disjoint_varnames :: "[vname list, (vname \<times> ty) list] \<Rightarrow> bool" where |
104 "disjoint_varnames pns lvars \<equiv> |
104 "disjoint_varnames pns lvars \<equiv> |
105 distinct pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> |
105 distinct pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> |
106 (\<forall>pn\<in>set pns. pn \<notin> set (map fst lvars))" |
106 (\<forall>pn\<in>set pns. pn \<notin> set (map fst lvars))" |