Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added BasisLibrary prefix to List.concat to avoid problems with
authorberghofe
Fri, 01 Jul 2005 14:10:02 +0200
changeset 16643 39cb9fe20fe3
parent 16642 849ec3962b55
child 16644 701218c1301c
Added BasisLibrary prefix to List.concat to avoid problems with modular code generation.
src/HOL/MicroJava/BV/BVExample.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/BV/BVExample.thy	Fri Jul 01 14:08:53 2005 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Fri Jul 01 14:10:02 2005 +0200
@@ -454,7 +454,7 @@
   "op :"   ("(_ mem _)")
   "op Un"  ("(_ union _)")
   "image"  ("map")
-  "UNION"  ("(fn A => fn f => List.concat (map f A))")
+  "UNION"  ("(fn A => fn f => BasisLibrary.List.concat (map f A))")
   "Bex"    ("(fn A => fn f => exists f A)")
   "Ball"   ("(fn A => fn f => forall f A)")
   "some_elem" ("hd")
@@ -475,7 +475,7 @@
 
 lemmas [code ind] = rtrancl_refl converse_rtrancl_into_rtrancl
 
-generate_code 
+generate_code
   test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0
     [(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"
   test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
isabelle