src/HOL/MicroJava/BV/BVExample.thy
changeset 15570 8d8c70b41bab
parent 15045 d59f7e2e18d3
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -454,7 +454,7 @@
     1.4    "op :"   ("(_ mem _)")
     1.5    "op Un"  ("(_ union _)")
     1.6    "image"  ("map")
     1.7 -  "UNION"  ("(fn A => fn f => flat (map f A))")
     1.8 +  "UNION"  ("(fn A => fn f => List.concat (map f A))")
     1.9    "Bex"    ("(fn A => fn f => exists f A)")
    1.10    "Ball"   ("(fn A => fn f => forall f A)")
    1.11    "some_elem" ("hd")