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*)