updated HOL-specific section w.r.t. datatypes
--- 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
--- 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},