# HG changeset patch
# User paulson
# Date 929274746 -7200
# Node ID 350f27e2d649a29cb341ee7dd3074582363f390b
# Parent  41d9b7bbf968e3bebe9d418f86997c63af52e3d9
guarantees -> juar

diff -r 41d9b7bbf968 -r 350f27e2d649 src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Fri Jun 11 17:14:00 1999 +0200
+++ b/src/HOL/UNITY/Client.ML	Sun Jun 13 13:52:26 1999 +0200
@@ -77,7 +77,7 @@
 
 (*Safety property 2: clients return the right number of tokens*)
 Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg))  \
-\               guarantees Always {s. rel s <= giv s}";
+\               guar Always {s. rel s <= giv s}";
 by (rtac guaranteesI 1);
 by (rtac AlwaysI 1);
 by (Force_tac 1);
@@ -104,7 +104,7 @@
 
 Goal "Cli_prg : \
 \      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \
-\      guarantees Always ({s. size (ask s) <= Suc (size (rel s))} Int \
+\      guar Always ({s. size (ask s) <= Suc (size (rel s))} Int \
 \                            {s. size (rel s) <= size (giv s)})";
 by (rtac guaranteesI 1);
 by (Clarify_tac 1);
@@ -124,7 +124,7 @@
 Goal "Cli_prg : \
 \      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
 \                 Int Always giv_meets_ask) \
-\      guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
+\      guar ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
 by (rtac guaranteesI 1);
 by (Clarify_tac 1);
 by (rtac Stable_transient_Always_LeadsTo 1);