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