Mercurial Mercurial > repos > Old_HOL / 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.
HOL/Trancl.thy: depends upon Prod
authorlcp
Fri, 19 Aug 1994 11:27:19 +0200
changeset 120 19facfd773de
parent 119 93dc86ccee28
child 121 2536dfe47b75
HOL/Trancl.thy: depends upon Prod
Trancl.thy file | annotate | diff | comparison | revisions 
--- a/Trancl.thy	Fri Aug 19 11:25:16 1994 +0200
+++ b/Trancl.thy	Fri Aug 19 11:27:19 1994 +0200
@@ -8,7 +8,7 @@
 rtrancl is refl/transitive closure;  trancl is transitive closure
 *)
 
-Trancl = Lfp +
+Trancl = Lfp + Prod + 
 consts
     trans   :: "('a * 'a)set => bool" 	(*transitivity predicate*)
     id	    :: "('a * 'a)set"
Old_HOL