src/HOL/UNITY/Comp/PriorityAux.thy
changeset 58860 fee7cfa69c50
parent 57284 886ff14f20cc
child 63146 f1ecba0272f9
     1.1 --- a/src/HOL/UNITY/Comp/PriorityAux.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -131,7 +131,7 @@
     1.4  done
     1.5  
     1.6  lemma above_lemma_b: 
     1.7 -     "acyclic r ==> above i r\<noteq>{}-->(\<exists>j \<in> above i r. above j r = {})";
     1.8 +     "acyclic r ==> above i r\<noteq>{}-->(\<exists>j \<in> above i r. above j r = {})"
     1.9  apply (drule above_lemma_a)
    1.10  apply (auto simp add: image0_trancl_iff_image0_r)
    1.11  done