# HG changeset patch
# User paulson
# Date 959960897 -7200
# Node ID b1f37f6819c42a4cafaf70861f18c5c17e43205a
# Parent  09d02e7365c16f54db117591ed46e938187d141f
new constant bag_of

diff -r 09d02e7365c1 -r b1f37f6819c4 src/HOL/UNITY/AllocBase.thy
--- a/src/HOL/UNITY/AllocBase.thy	Fri Jun 02 17:47:41 2000 +0200
+++ b/src/HOL/UNITY/AllocBase.thy	Fri Jun 02 17:48:17 2000 +0200
@@ -5,10 +5,11 @@
 
 Common declarations for Chandy and Charpentier's Allocator
 
-with_path "../Induct" time_use_thy "AllocBase";
+add_path "../Induct";
+time_use_thy "AllocBase";
 *)
 
-AllocBase = Rename + Follows + MultisetOrder +
+AllocBase = Rename + Follows + 
 
 consts
   NbT      :: nat       (*Number of tokens in system*)
@@ -32,4 +33,12 @@
 constdefs sublist :: "['a list, nat set] => 'a list"
     "sublist l A == map fst (filter (%p. snd p : A) (zip l [0..size l(]))"
 
+
+consts
+  bag_of :: 'a list => 'a multiset
+
+primrec
+  "bag_of []     = {#}"
+  "bag_of (x#xs) = {#x#} + bag_of xs"
+
 end