# HG changeset patch
# User paulson
# Date 904725409 -7200
# Node ID c57c87628bb4e10f4ab8028e913d8953b7de7a9b
# Parent  578dc167453f6cbafe489cfd46f4b924eaba35ca
two new thms

diff -r 578dc167453f -r c57c87628bb4 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];