src/HOL/IOA/NTP/Multiset.thy
changeset 1376 92f83b9d17e1
parent 1328 9a449a91425d
--- a/src/HOL/IOA/NTP/Multiset.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Multiset.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -19,11 +19,11 @@
 
 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"
+  "{|}"  :: '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