Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Inductive.ML
changeset 4970 8b65444edbb0
parent 4872 33e7cdc20681 
--- a/src/HOL/Inductive.ML	Wed May 27 12:19:35 1998 +0200
+++ b/src/HOL/Inductive.ML	Wed May 27 12:21:39 1998 +0200
@@ -18,7 +18,7 @@
 
 structure Lfp_items =
   struct
-  val checkThy	= (fn thy => Theory.require thy "Lfp" "inductive definitions")
+  val checkThy	= (fn thy => Theory.requires thy "Lfp" "inductive definitions")
   val oper      = gen_fp_oper "lfp"
   val Tarski    = def_lfp_Tarski
   val induct    = def_induct
@@ -26,7 +26,7 @@
 
 structure Gfp_items =
   struct
-  val checkThy	= (fn thy => Theory.require thy "Gfp" "coinductive definitions")
+  val checkThy	= (fn thy => Theory.requires thy "Gfp" "coinductive definitions")
   val oper      = gen_fp_oper "gfp"
   val Tarski    = def_gfp_Tarski
   val induct    = def_Collect_coinduct
isabelle