diff -r 741deccec4e3 -r bca33c49b083 src/ZF/UNITY/ClientImpl.thy --- 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 *)