src/HOLCF/ex/Pattern_Match.thy

 
 subsection {* ML code for generating definitions *}
 
 ML {*
 local open HOLCF_Library in
+
+infixr 6 ->>;
+infix 9 ` ;
 
 val beta_rules =
   @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @
   @{thms cont2cont_fst cont2cont_snd cont2cont_Pair};