src/HOL/ex/Classpackage.thy
changeset 21460 cda5cd8bfd16
parent 21404 eb85850d3eb7
child 21545 54cc492d80a9
     1.1 --- a/src/HOL/ex/Classpackage.thy	Wed Nov 22 10:20:19 2006 +0100
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Wed Nov 22 10:20:20 2006 +0100
     1.3 @@ -320,10 +320,7 @@
     1.4  definition "y2 = Y (1::int) 2 3"
     1.5  
     1.6  code_gen "op \<otimes>" \<one> inv
     1.7 -code_gen X Y (SML) (Haskell)
     1.8 -code_gen x1 x2 y2 (SML) (Haskell)
     1.9 -
    1.10 -code_gen (SML *)
    1.11 -code_gen (Haskell -)
    1.12 +code_gen X Y (SML *) (Haskell -)
    1.13 +code_gen x1 x2 y2 (SML *) (Haskell -)
    1.14  
    1.15  end