# HG changeset patch
# User blanchet
# Date 1410177782 -7200
# Node ID cccf5445e2245b7f97a5749a6a471899c565464c
# Parent  bd17543779654e893db2efc8b7ba16d800447d32
tuned docs

diff -r bd1754377965 -r cccf5445e224 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 08 14:03:01 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 08 14:03:02 2014 +0200
@@ -615,7 +615,8 @@
 
 \item The old-style, nested-as-mutual induction rule and recursor theorems are
 generated under their usual names but with ``@{text "compat_"}'' prefixed
-(e.g., @{text compat_tree.induct}).
+(e.g., @{text compat_tree.induct}, @{text compat_tree.inducts}, and
+@{text compat_tree.rec}).
 
 \item All types through which recursion takes place must be new-style datatypes
 or the function type. In principle, it should be possible to support old-style