src/ZF/UNITY/ClientImpl.thy
changeset 24892 c663e675e177
parent 24051 896fb015079c
child 24893 b8ef7afe3a6b
     1.1 --- a/src/ZF/UNITY/ClientImpl.thy	Sun Oct 07 13:57:05 2007 +0200
     1.2 +++ b/src/ZF/UNITY/ClientImpl.thy	Sun Oct 07 15:49:25 2007 +0200
     1.3 @@ -6,20 +6,12 @@
     1.4  Distributed Resource Management System:  Client Implementation
     1.5  *)
     1.6  
     1.7 -
     1.8  theory ClientImpl imports AllocBase Guar begin
     1.9  
    1.10 -consts
    1.11 -  ask :: i (* input history:  tokens requested *)
    1.12 -  giv :: i (* output history: tokens granted *)
    1.13 -  rel :: i (* input history: tokens released *)
    1.14 -  tok :: i (* the number of available tokens *)
    1.15 -
    1.16 -translations
    1.17 -  "ask" == "Var(Nil)"
    1.18 -  "giv" == "Var([0])"
    1.19 -  "rel" == "Var([1])"
    1.20 -  "tok" == "Var([2])"
    1.21 +abbreviation "ask == Var(Nil)" (* input history:  tokens requested *)
    1.22 +abbreviation "giv == Var([0])" (* output history: tokens granted *)
    1.23 +abbreviation "rel == Var([1])" (* input history: tokens released *)
    1.24 +abbreviation "tok == Var([2])" (* the number of available tokens *)
    1.25  
    1.26  axioms
    1.27    type_assumes: