src/HOL/List.thy
changeset 47433 07f4bf913230
parent 47131 af818dcdc709
child 47436 d8fad618a67a
     1.1 --- a/src/HOL/List.thy	Tue Apr 03 08:55:06 2012 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Apr 03 17:26:30 2012 +0900
     1.3 @@ -5747,7 +5747,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