# HG changeset patch
# User krauss
# Date 1306523504 -7200
# Node ID 0f9534b7ea752768886daafa6a31ea547eac5d07
# Parent  218e3943d50418d1e0c5eb2fb98f395c47ff3d0f
function tutorial: do not omit termination proof, even when discussing other things

diff -r 218e3943d504 -r 0f9534b7ea75 doc-src/Functions/Thy/Functions.thy
--- a/doc-src/Functions/Thy/Functions.thy	Fri May 27 16:45:24 2011 +0200
+++ b/doc-src/Functions/Thy/Functions.thy	Fri May 27 21:11:44 2011 +0200
@@ -558,6 +558,7 @@
 *}
 
 by auto
+termination by (relation "{}") simp
 
 
 subsection {* Non-constructor patterns *}
@@ -685,6 +686,7 @@
   "check (''good'') = True"
 | "s \<noteq> ''good'' \<Longrightarrow> check s = False"
 by auto
+termination by (relation "{}") simp
 
 
 section {* Partiality *}
diff -r 218e3943d504 -r 0f9534b7ea75 doc-src/Functions/Thy/document/Functions.tex
--- a/doc-src/Functions/Thy/document/Functions.tex	Fri May 27 16:45:24 2011 +0200
+++ b/doc-src/Functions/Thy/document/Functions.tex	Fri May 27 21:11:44 2011 +0200
@@ -803,6 +803,22 @@
 \isadelimproof
 %
 \endisadelimproof
+\isanewline
+\isacommand{termination}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}relation\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
 %
 \isamarkupsubsection{Non-constructor patterns%
 }
@@ -1039,6 +1055,22 @@
 {\isafoldproof}%
 %
 \isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{termination}\isamarkupfalse%
+%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}relation\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
 %
 \endisadelimproof
 %