src/HOL/Induct/ROOT.ML
changeset 5078 7b5ea59c0275
parent 4449 df30e75f670f
child 5417 1f533238b53b
--- a/src/HOL/Induct/ROOT.ML	Wed Jun 24 13:59:45 1998 +0200
+++ b/src/HOL/Induct/ROOT.ML	Thu Jun 25 13:57:34 1998 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 
-Exampled of Inductive Definitions
+Examples of Inductive and Coinductive Definitions
 *)
 
 HOL_build_completed;    (*Make examples fail if HOL did*)