Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Theory.require;
authorwenzelm
Wed, 29 Apr 1998 11:33:06 +0200
changeset 4856 802c1f9ec156
parent 4855 62bc389d6168
child 4857 cf554f1c65be
Theory.require;
TFL/post.sml file | annotate | diff | comparison | revisions 
--- a/TFL/post.sml	Wed Apr 29 11:30:55 1998 +0200
+++ b/TFL/post.sml	Wed Apr 29 11:33:06 1998 +0200
@@ -84,7 +84,7 @@
  * Defining a function with an associated termination relation. 
  *---------------------------------------------------------------------------*)
 fun define_i thy fid R eqs = 
-  let val dummy = require_thy thy "WF_Rel" "recursive function definitions"
+  let val dummy = Theory.require thy "WF_Rel" "recursive function definitions"
       val {functional,pats} = Prim.mk_functional thy eqs
   in (Prim.wfrec_definition0 thy fid R functional, pats)
   end;
isabelle