# HG changeset patch
# User blanchet
# Date 1411979979 -7200
# Node ID 330ebcc3e77d33bdd652da25161f2f55dc21a7f1
# Parent  d919cde2569147f8e47361a715019e8dbfa1e285
reintroduced 'rel_cases' in docs

diff -r d919cde25691 -r 330ebcc3e77d src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 29 10:39:39 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 29 10:39:39 2014 +0200
@@ -900,9 +900,8 @@
 @{thm list.rel_intros(1)[no_vars]} \\
 @{thm list.rel_intros(2)[no_vars]}
 
-% FIXME (and add @ before antiquotation below)
-%\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\
-%{thm list.rel_cases[no_vars]}
+\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\
+@{thm list.rel_cases[no_vars]}
 
 \item[@{text "t."}\hthm{rel_sel}\rm:] ~ \\
 @{thm list.rel_sel[no_vars]}