| changeset 63040 | eb4ddd18d635 |
| parent 60304 | 3f429b7d8eb5 |
| child 69085 | 9999d7823b8f |
--- a/src/HOL/MicroJava/Comp/Index.thy Sun Apr 24 21:31:14 2016 +0200 +++ b/src/HOL/MicroJava/Comp/Index.thy Mon Apr 25 16:09:26 2016 +0200 @@ -98,7 +98,7 @@ -(* The following def should replace the conditions in WellType.thy / wf_java_mdecl +(* The following definition should replace the conditions in WellType.thy / wf_java_mdecl *) definition disjoint_varnames :: "[vname list, (vname \<times> ty) list] \<Rightarrow> bool" where "disjoint_varnames pns lvars \<equiv>