changeset 4423 | a129b817b58a |
parent 4283 | 92707e24b62b |
child 4477 | b3e5857d8d99 |
--- a/src/HOLCF/IOA/meta_theory/Traces.ML Tue Dec 16 15:17:26 1997 +0100 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML Tue Dec 16 17:58:03 1997 +0100 @@ -197,7 +197,7 @@ "!! A.[| x:traces A |] ==> \ \ Forall (%a. a:act A) x"; by (safe_tac set_cs ); -br ForallQFilterP 1; +by (rtac ForallQFilterP 1); by (fast_tac (!claset addSIs [ext_is_act]) 1); qed"traces_in_sig"; *)