# HG changeset patch
# User blanchet
# Date 1454367126 -3600
# Node ID a00306a1c71ae80ca78952dcbc05db3a6c23ad6a
# Parent  614d88f87cfe853cbe00341545ec4b9934b7cdf7
updated HOL-specific section w.r.t. datatypes

diff -r 614d88f87cfe -r a00306a1c71a src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Tue Feb 02 15:04:39 2016 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Feb 01 23:52:06 2016 +0100
@@ -642,14 +642,15 @@
   \<close>}
 
   \<^descr> @{command (HOL) "recdef"} defines general well-founded
-  recursive functions (using the TFL package), see also
-  @{cite "isabelle-HOL"}.  The ``\<open>(permissive)\<close>'' option tells
-  TFL to recover from failed proof attempts, returning unfinished
-  results.  The \<open>recdef_simp\<close>, \<open>recdef_cong\<close>, and \<open>recdef_wf\<close> hints refer to auxiliary rules to be used in the internal
-  automated proof process of TFL.  Additional @{syntax clasimpmod}
-  declarations may be given to tune the context of the Simplifier
-  (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\
-  \secref{sec:classical}).
+  recursive functions (using the TFL package).  The
+  ``\<open>(permissive)\<close>'' option tells TFL to recover from
+  failed proof attempts, returning unfinished results.  The
+  \<open>recdef_simp\<close>, \<open>recdef_cong\<close>, and
+  \<open>recdef_wf\<close> hints refer to auxiliary rules to be used
+  in the internal automated proof process of TFL.  Additional
+  @{syntax clasimpmod} declarations may be given to tune the context
+  of the Simplifier (cf.\ \secref{sec:simplifier}) and Classical
+  reasoner (cf.\ \secref{sec:classical}).
 
 
   \<^medskip>
@@ -763,9 +764,8 @@
   These commands are mostly obsolete; @{command (HOL) "datatype"}
   should be used instead.
 
-  See @{cite "isabelle-HOL"} for more details on datatypes, but beware of
-  the old-style theory syntax being used there!  Apart from proper
-  proof methods for case-analysis and induction, there are also
+  See @{cite "isabelle-datatypes"} for more details on datatypes.  Apart from proper
+  proof methods for case analysis and induction, there are also
   emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)
   induct_tac} available, see \secref{sec:hol-induct-tac}; these admit
   to refer directly to the internal structure of subgoals (including
diff -r 614d88f87cfe -r a00306a1c71a src/Doc/manual.bib
--- a/src/Doc/manual.bib	Tue Feb 02 15:04:39 2016 +0100
+++ b/src/Doc/manual.bib	Mon Feb 01 23:52:06 2016 +0100
@@ -306,6 +306,12 @@
   series = 	 LNCS,
   publisher = Springer}
 
+@manual{isabelle-datatypes,
+  author	= {Julian Biendarra and Jasmin Christian Blanchette and Martin Desharnais and Lorenz Panny and Andrei Popescu and Dmitriy Traytel},
+  title		= {Defining (Co)datatypes and Primitively (Co)recursive Functions in {Isabelle\slash HOL}},
+  institution	= {TU Munich},
+  note          = {\url{http://isabelle.in.tum.de/doc/datatypes.pdf}}}
+
 @book{Bird-Wadler,author="Richard Bird and Philip Wadler",
 title="Introduction to Functional Programming",publisher=PH,year=1988}
 
@@ -373,12 +379,6 @@
   pages = "93--110"
 }
 
-@manual{isabelle-datatypes,
-  author	= {Jasmin Christian Blanchette and Martin Desharnais and Lorenz Panny and Andrei Popescu and Dmitriy Traytel},
-  title		= {Defining (Co)datatypes in Isabelle/HOL},
-  institution	= {TU Munich},
-  note          = {\url{http://isabelle.in.tum.de/doc/datatypes.pdf}}}
-
 @inproceedings{why3,
   author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
   title = {{Why3}: Shepherd Your Herd of Provers},