IOA/example/Multiset.ML
changeset 168 44ff2275d44f
parent 156 fd1be45b64bf
child 171 16c4ea954511
equal deleted inserted replaced
167:37a6e2f55230 168:44ff2275d44f
       
     1 (*  Title:      HOL/IOA/example/Multiset.ML
       
     2     ID:         $Id$
       
     3     Author:     Tobias Nipkow & Konrad Slind
       
     4     Copyright   1994  TU Muenchen
       
     5 
       
     6 Axiomatic multisets.
       
     7 Should be done as a subtype and moved to a global place.
       
     8 *)
       
     9 
     1 goalw Multiset.thy [Multiset.count_def, Multiset.countm_empty_def]
    10 goalw Multiset.thy [Multiset.count_def, Multiset.countm_empty_def]
     2    "count({|},x) = 0";
    11    "count({|},x) = 0";
     3  by (rtac refl 1);
    12  by (rtac refl 1);
     4 val count_empty = result();
    13 val count_empty = result();
     5 
    14