src/HOL/ex/Classpackage.thy
changeset 22845 5f9138bcb3d7
parent 22473 753123c89d72
child 23810 f5e6932d0500
     1.1 --- a/src/HOL/ex/Classpackage.thy	Sun May 06 21:49:44 2007 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Sun May 06 21:50:17 2007 +0200
     1.3 @@ -338,7 +338,6 @@
     1.4  definition "x2 = X (1::int) 2 3"
     1.5  definition "y2 = Y (1::int) 2 3"
     1.6  
     1.7 -code_gen "op \<otimes>" \<one> inv X Y
     1.8 -code_gen x1 x2 y2 (SML #) (OCaml -) (Haskell -)
     1.9 +code_gen x1 x2 y2 in SML in OCaml file - in Haskell file -
    1.10  
    1.11  end