changeset 10138 | 412a3ced6efd |
parent 10061 | fe82134773dc |
child 10613 | 78b1d6c3ee9c |
--- a/src/HOL/MicroJava/J/TypeRel.thy Tue Oct 03 18:40:25 2000 +0200 +++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Oct 03 18:44:19 2000 +0200 @@ -52,7 +52,7 @@ "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => empty | Some (sc,fs,ms) => (case sc of None => empty | Some D => if is_class G D then method (G,D) - else arbitrary) \\<oplus> + else arbitrary) ++ map_of (map (\\<lambda>(s, m ). (s,(C,m))) ms)) else arbitrary)"