--- a/src/HOLCF/IOA/meta_theory/Traces.ML Tue Nov 25 16:34:20 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Tue Nov 25 17:56:49 1997 +0100
@@ -189,6 +189,19 @@
by (fast_tac (claset() addSIs [exec_in_sig]) 1);
qed"scheds_in_sig";
+(*
+
+is ok but needs ForallQFilterP which has to been proven first (is trivial also)
+
+goalw thy [traces_def,has_trace_def]
+ "!! A.[| x:traces A |] ==> \
+\ Forall (%a. a:act A) x";
+ by (safe_tac set_cs );
+br ForallQFilterP 1;
+by (fast_tac (!claset addSIs [ext_is_act]) 1);
+qed"traces_in_sig";
+*)
+
(* -------------------------------------------------------------------------------- *)