NEWS
changeset 37417 037ee7b712b2
parent 37408 a2a89563bfcb
child 37484 b7821e89fb79
equal deleted inserted replaced
37416:69ba3f21c295 37417:037ee7b712b2
    32 (class eq) carry proper names and are treated as default code
    32 (class eq) carry proper names and are treated as default code
    33 equations.
    33 equations.
    34 
    34 
    35 * List.thy: use various operations from the Haskell prelude when
    35 * List.thy: use various operations from the Haskell prelude when
    36 generating Haskell code.
    36 generating Haskell code.
       
    37 
       
    38 * code_simp.ML: simplification with rules determined by
       
    39 code generator.
       
    40 
       
    41 * code generator: do not print function definitions for case
       
    42 combinators any longer.
    37 
    43 
    38 
    44 
    39 
    45 
    40 New in Isabelle2009-2 (June 2010)
    46 New in Isabelle2009-2 (June 2010)
    41 ---------------------------------
    47 ---------------------------------