doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 37420 1cf6f134e7f2
parent 36453 2f383885d8f8
child 37422 6d19e4e6ebf5
equal deleted inserted replaced
37409:6c9f23863808 37420:1cf6f134e7f2
  1080     ;
  1080     ;
  1081 
  1081 
  1082     target: 'OCaml' | 'SML' | 'Haskell'
  1082     target: 'OCaml' | 'SML' | 'Haskell'
  1083     ;
  1083     ;
  1084 
  1084 
  1085     'code\_datatype' const +
  1085     'code\_datatype' ( const + )
  1086     ;
  1086     ;
  1087 
  1087 
  1088     'code\_const' (const + 'and') \\
  1088     'code\_const' (const + 'and') \\
  1089       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  1089       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  1090     ;
  1090     ;