two new thms
authorpaulson
Wed, 02 Sep 1998 10:36:49 +0200
changeset 5423 c57c87628bb4
parent 5422 578dc167453f
child 5424 771a68a468cc
two new thms
src/HOL/UNITY/Traces.ML
--- a/src/HOL/UNITY/Traces.ML	Wed Sep 02 10:36:22 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML	Wed Sep 02 10:36:49 1998 +0200
@@ -20,3 +20,12 @@
 by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
 qed "stable_reachable";
 
+Goal "(act : Acts(|Init=init, Acts=acts|)) = (act:acts)";
+auto();
+qed "Acts_eq";
+
+Goal "(s : Init(|Init=init, Acts=acts|)) = (s:init)";
+auto();
+qed "Init_eq";
+
+AddIffs [Acts_eq, Init_eq];