# 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);