| changeset 5423 | c57c87628bb4 |
| parent 5313 | 1861a564d7e2 |
| child 5426 | 566f47250bd0 |
--- 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];