src/HOLCF/IOA/meta_theory/Traces.ML
changeset 4283 92707e24b62b
parent 4098 71e05eb27fb6
child 4423 a129b817b58a
--- 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";
+*)
+
 
 (* -------------------------------------------------------------------------------- *)