1.1 --- a/src/HOL/UNITY/AllocBase.thy	Fri Jun 02 17:47:41 2000 +0200
     1.2 +++ b/src/HOL/UNITY/AllocBase.thy	Fri Jun 02 17:48:17 2000 +0200
     1.3 @@ -5,10 +5,11 @@
     1.4  
     1.5  Common declarations for Chandy and Charpentier's Allocator
     1.6  
     1.7 -with_path "../Induct" time_use_thy "AllocBase";
     1.8 +add_path "../Induct";
     1.9 +time_use_thy "AllocBase";
    1.10  *)
    1.11  
    1.12 -AllocBase = Rename + Follows + MultisetOrder +
    1.13 +AllocBase = Rename + Follows + 
    1.14  
    1.15  consts
    1.16    NbT      :: nat       (*Number of tokens in system*)
    1.17 @@ -32,4 +33,12 @@
    1.18  constdefs sublist :: "['a list, nat set] => 'a list"
    1.19      "sublist l A == map fst (filter (%p. snd p : A) (zip l [0..size l(]))"
    1.20  
    1.21 +
    1.22 +consts
    1.23 +  bag_of :: 'a list => 'a multiset
    1.24 +
    1.25 +primrec
    1.26 +  "bag_of []     = {#}"
    1.27 +  "bag_of (x#xs) = {#x#} + bag_of xs"
    1.28 +
    1.29  end