--- a/src/ZF/UNITY/AllocBase.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/AllocBase.thy Sun Oct 07 15:49:25 2007 +0200
@@ -10,11 +10,13 @@
theory AllocBase imports Follows MultisetSum Guar begin
consts
- tokbag :: i (* tokbags could be multisets...or any ordered type?*)
NbT :: i (* Number of tokens in system *)
Nclients :: i (* Number of clients *)
-translations "tokbag" => "nat"
+abbreviation (input)
+ tokbag :: i (* tokbags could be multisets...or any ordered type?*)
+where
+ "tokbag == nat"
axioms
NbT_pos: "NbT \<in> nat-{0}"