--- a/src/ZF/UNITY/ClientImpl.thy Mon Jun 30 12:23:00 2003 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy Mon Jun 30 18:15:51 2003 +0200
@@ -9,7 +9,7 @@
theory ClientImpl = AllocBase + Guar:
-(*????MOVE UP*)
+(*move to Constrains.thy when the latter is converted to Isar format*)
method_setup constrains = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
@@ -17,13 +17,6 @@
Simplifier.get_local_simpset ctxt) 1)) *}
"for proving safety properties"
-(*For using "disjunction" (union over an index set) to eliminate a variable.
- ????move way up*)
-lemma UN_conj_eq: "\<forall>s\<in>state. f(s) \<in> A
- ==> (\<Union>k\<in>A. {s\<in>state. P(s) & f(s) = k}) = {s\<in>state. P(s)}"
-by blast
-
-
consts
ask :: i (* input history: tokens requested *)
giv :: i (* output history: tokens granted *)