src/HOL/Induct/Multiset0.ML
author paulson
Wed Mar 03 11:15:18 1999 +0100 (1999-03-03)
changeset 6301 08245f5a436d
parent 5628 15b7f12ad919
child 8935 548901d05a0e
permissions -rw-r--r--
expandshort
nipkow@5628
     1
(*  Title:      HOL/Induct/Multiset0.ML
nipkow@5628
     2
    ID:         $Id$
nipkow@5628
     3
    Author:     Tobias Nipkow
nipkow@5628
     4
    Copyright   1998 TUM
nipkow@5628
     5
nipkow@5628
     6
This theory merely proves that the representation of multisets is nonempty.
nipkow@5628
     7
*)
nipkow@5628
     8
nipkow@5628
     9
Goal "(%x.0) : {f. finite {x. 0 < f x}}";
paulson@6301
    10
by (Simp_tac 1);
nipkow@5628
    11
qed "multiset_witness";