--- 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