src/HOL/List.thy
changeset 47436 d8fad618a67a
parent 47399 b72fa7bf9a10
parent 47433 07f4bf913230
child 47640 62bfba15b212
     1.1 --- a/src/HOL/List.thy	Thu Apr 12 10:13:33 2012 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Apr 12 11:01:15 2012 +0200
     1.3 @@ -5677,7 +5677,7 @@
     1.4    "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)"
     1.5    by (simp add: finite_trancl_ntranl)
     1.6  
     1.7 -lemma set_rel_comp [code]:
     1.8 +lemma set_relcomp [code]:
     1.9    "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
    1.10    by (auto simp add: Bex_def)
    1.11