--- a/doc-src/TutorialI/Types/Overloading.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading.thy Sat Dec 01 18:52:32 2001 +0100
@@ -1,13 +1,13 @@
(*<*)theory Overloading = Overloading1:(*>*)
-instance list :: ("term")ordrel
+instance list :: (type)ordrel
by intro_classes
text{*\noindent
This \isacommand{instance} declaration can be read like the declaration of
a function on types. The constructor @{text list} maps types of class @{text
-term} (all HOL types), to types of class @{text ordrel};
+type} (all HOL types), to types of class @{text ordrel};
in other words,
-if @{text"ty :: term"} then @{text"ty list :: ordrel"}.
+if @{text"ty :: type"} then @{text"ty list :: ordrel"}.
Of course we should also define the meaning of @{text <<=} and
@{text <<} on lists:
*}