
diff -r f04b33ce250f -r a4dc62a46ee4 IOA/example/Multiset.thy
--- a/IOA/example/Multiset.thy	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(*  Title:      HOL/IOA/example/Multiset.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow & Konrad Slind
-    Copyright   1994  TU Muenchen
-
-Axiomatic multisets.
-Should be done as a subtype and moved to a global place.
-*)
-
-Multiset = Arith + "Lemmas" +
-
-types
-
-  'a multiset
-
-arities
-
-  multiset :: (term) term
-
-consts
-
-  "{|}"  :: "'a multiset"                        ("{|}")
-  addm   :: "['a multiset, 'a] => 'a multiset"
-  delm   :: "['a multiset, 'a] => 'a multiset"
-  countm :: "['a multiset, 'a => bool] => nat"
-  count  :: "['a multiset, 'a] => nat"
-
-rules
-
-delm_empty_def
-  "delm({|},x) = {|}" 
-
-delm_nonempty_def
-  "delm(addm(M,x),y) == if(x=y,M,addm(delm(M,y),x))"
-
-countm_empty_def
-   "countm({|},P) == 0"
-
-countm_nonempty_def
-   "countm(addm(M,x),P) == countm(M,P) + if(P(x), Suc(0), 0)"
-
-count_def
-   "count(M,x) == countm(M, %y.y = x)"
-
-induction
-   "[| P({|}); !!M x. P(M) ==> P(addm(M,x)) |] ==> P(M)"
-
-end




