src/HOLCF/Fixrec.thy
changeset 35469 6e59de61d501
parent 35115 446c5063e4fd
child 35527 f4282471461d
equal deleted inserted replaced
35468:09bc6a2e2296 35469:6e59de61d501
   263 
   263 
   264   in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
   264   in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
   265 *}
   265 *}
   266 
   266 
   267 translations
   267 translations
   268   "x" <= "_match Fixrec.return (_variable x)"
   268   "x" <= "_match (CONST Fixrec.return) (_variable x)"
   269 
   269 
   270 
   270 
   271 subsection {* Pattern combinators for data constructors *}
   271 subsection {* Pattern combinators for data constructors *}
   272 
   272 
   273 types ('a, 'b) pat = "'a \<rightarrow> 'b maybe"
   273 types ('a, 'b) pat = "'a \<rightarrow> 'b maybe"