src/HOL/Tools/BNF/bnf_fp_util.ML

   val map_uniqueN: string
   val min_algN: string
   val morN: string
   val nchotomyN: string
   val recN: string
+  val rel_casesN: string
   val rel_coinductN: string
   val rel_inductN: string
   val rel_injectN: string
   val rel_introsN: string
   val rel_distinctN: string

 val iffN = "_iff"
 val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
 val distinctN = "distinct"
 val rel_distinctN = relN ^ "_" ^ distinctN
 val injectN = "inject"
+val rel_casesN = relN ^ "_cases"
 val rel_injectN = relN ^ "_" ^ injectN
 val rel_introsN = relN ^ "_intros"
 val rel_coinductN = relN ^ "_" ^ coinductN
 val dtor_rel_coinductN = dtorN ^ "_" ^ rel_coinductN
 val rel_inductN = relN ^ "_" ^ inductN