--- a/doc-src/TutorialI/Recdef/Nested1.thy Wed Oct 18 12:30:59 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Wed Oct 18 17:19:18 2000 +0200
@@ -21,7 +21,7 @@
Remember that function @{term size} is defined for each \isacommand{datatype}.
However, the definition does not succeed. Isabelle complains about an
unproved termination condition
-@{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
+@{prop[display]"t : set ts --> size t < Suc (term_list_size ts)"}
where @{term set} returns the set of elements of a list
and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
function automatically defined by Isabelle