# HG changeset patch
# User paulson
# Date 907925126 -7200
# Node ID 707f30bc7fe756ca4555c6171ad2ebde0822543d
# Parent  fc2c299187c01f249b636d8a02dfc53a8b846a59
new theorems

diff -r fc2c299187c0 -r 707f30bc7fe7 src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Fri Oct 09 11:24:46 1998 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Fri Oct 09 11:25:26 1998 +0200
@@ -20,11 +20,14 @@
 	  rewrite_rule [stable_def] stable_reachable RS 
 	  constrains_Int);
 
-Goalw [Constrains_def]
-    "constrains (Acts F) A A' ==> Constrains F A A'";
+Goalw [Constrains_def] "constrains (Acts F) A A' ==> Constrains F A A'";
 by (etac constrains_reachable_Int 1);
 qed "constrains_imp_Constrains";
 
+Goalw [stable_def, Stable_def] "stable (Acts F) A ==> Stable F A";
+by (etac constrains_imp_Constrains 1);
+qed "stable_imp_Stable";
+
 val prems = Goal
     "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A') \
 \    ==> Constrains F A A'";