src/HOL/Predicate.thy
changeset 23708 b5eb0b4dd17d
parent 23389 aaca6a8e5414
child 23741 1801a921df13
--- a/src/HOL/Predicate.thy	Tue Jul 10 17:30:47 2007 +0200
+++ b/src/HOL/Predicate.thy	Tue Jul 10 17:30:49 2007 +0200
@@ -6,7 +6,7 @@
 header {* Predicates *}
 
 theory Predicate
-imports Inductive
+imports Inductive Relation
 begin
 
 subsection {* Converting between predicates and sets *}