Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/UNITY/ClientImpl.thy
changeset 41779 a68f503805ed
parent 32960 69916a850301
child 46823 57bf0cecb366 
--- a/src/ZF/UNITY/ClientImpl.thy	Fri Feb 18 16:36:42 2011 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy	Fri Feb 18 17:03:30 2011 +0100
@@ -12,13 +12,13 @@
 abbreviation "rel == Var([1])" (* input history: tokens released *)
 abbreviation "tok == Var([2])" (* the number of available tokens *)
 
-axioms
+axiomatization where
   type_assumes:
   "type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) & 
-   type_of(rel) = list(tokbag) & type_of(tok) = nat"
+   type_of(rel) = list(tokbag) & type_of(tok) = nat" and
   default_val_assumes:
-  "default_val(ask) = Nil & default_val(giv)  = Nil & 
-   default_val(rel)  = Nil & default_val(tok)  = 0"
+  "default_val(ask) = Nil & default_val(giv) = Nil & 
+   default_val(rel) = Nil & default_val(tok) = 0"
 
 
 (*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *)
isabelle