src/HOL/Bali/Basis.thy
changeset 12893 cbb4dc5e6478
parent 12859 f63315dfffd4
child 12919 d6a0d168291e
     1.1 --- a/src/HOL/Bali/Basis.thy	Fri Feb 15 20:41:19 2002 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Fri Feb 15 20:41:39 2002 +0100
     1.3 @@ -280,7 +280,7 @@
     1.4  
     1.5  constdefs
     1.6    unique   :: "('a \<times> 'b) list \<Rightarrow> bool"
     1.7 - "unique \<equiv> nodups \<circ> map fst"
     1.8 + "unique \<equiv> distinct \<circ> map fst"
     1.9  
    1.10  lemma uniqueD [rule_format (no_asm)]: 
    1.11  "unique l--> (!x y. (x,y):set l --> (!x' y'. (x',y'):set l --> x=x'-->  y=y'))"