Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Finite_Set.thy
changeset 14443 75910c7557c5
parent 14430 5cb24165a2e1
child 14449 d5c3d21df790
equal deleted inserted replaced
14442:04135b0c06ff 14443:75910c7557c5 
  1421 
  1421 
  1422 theorem n_subsets:
 
  1422 theorem n_subsets:
 
  1423     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
 
  1423     "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
 
  1424   by (simp add: n_sub_lemma)
 
  1424   by (simp add: n_sub_lemma)
 
  1425 
  1425 
       
  1426 
  1426 end
 
  1427 end
isabelle