--- a/src/ZF/UNITY/ClientImpl.thy Sat Mar 26 18:20:29 2005 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy Mon Mar 28 16:19:56 2005 +0200
@@ -9,13 +9,6 @@
theory ClientImpl = AllocBase + Guar:
-(*move to Constrains.thy when the latter is converted to Isar format*)
-method_setup constrains = {*
- Method.ctxt_args (fn ctxt =>
- Method.METHOD (fn facts =>
- gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
- "for proving safety properties"
-
consts
ask :: i (* input history: tokens requested *)
giv :: i (* output history: tokens granted *)