src/HOL/Wellfounded.thy
changeset 61943 7fba644ed827
parent 61799 4cf66f21b764
child 61952 546958347e05
     1.1 --- a/src/HOL/Wellfounded.thy	Sun Dec 27 21:46:36 2015 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Sun Dec 27 22:07:17 2015 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  text\<open>Restriction to domain @{term A} and range @{term B}.  If @{term r} is
     1.5      well-founded over their intersection, then @{term "wf r"}\<close>
     1.6  lemma wfI: 
     1.7 - "[| r \<subseteq> A <*> B; 
     1.8 + "[| r \<subseteq> A \<times> B; 
     1.9       !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x;  x : A; x : B |] ==> P x |]
    1.10    ==>  wf r"
    1.11    unfolding wf_def by blast