| changeset 14134 | 0fdf5708c7a8 |
| parent 12951 | a9fdcb71d252 |
| child 16417 | 9bc16273c2d4 |
--- a/src/HOL/MicroJava/J/Decl.thy Fri Jul 25 10:52:15 2003 +0200 +++ b/src/HOL/MicroJava/J/Decl.thy Fri Jul 25 17:21:22 2003 +0200 @@ -33,7 +33,7 @@ constdefs - class :: "'c prog => (cname \<leadsto> 'c class)" + class :: "'c prog => (cname \<rightharpoonup> 'c class)" "class \<equiv> map_of" is_class :: "'c prog => cname => bool"