src/HOL/Finite.thy

   EmptyI  "({},0) : cardR"
   InsertI "[| (A,n) : cardR; a ~: A |] ==> (insert a A, Suc n) : cardR"
 
 constdefs
   card :: 'a set => nat
- "card A == @n. (A,n) : cardR"
+ "card A == THE n. (A,n) : cardR"
 
 (*
 A "fold" functional for finite sets.  For n non-negative we have
     fold f e {x1,...,xn} = f x1 (... (f xn e))
 where f is at least left-commutative.

     insertI  "[| x ~: A;  (A,y) : foldSet f e |]
 	      ==> (insert x A, f x y) : foldSet f e"
 
 constdefs
    fold :: "[['b,'a] => 'a, 'a, 'b set] => 'a"
-  "fold f e A == @x. (A,x) : foldSet f e"
+  "fold f e A == THE x. (A,x) : foldSet f e"
 
    setsum :: "('a => 'b) => 'a set => ('b::{plus, zero})"
   "setsum f A == if finite A then fold (op+ o f) 0 A else 0"
 
 locale LC =