changeset 7537 | 875754b599df |
parent 7361 | 477e1bdf230f |
child 7594 | 8a188ef6545e |
--- a/src/HOL/UNITY/Client.ML Fri Sep 10 18:37:04 1999 +0200 +++ b/src/HOL/UNITY/Client.ML Fri Sep 10 18:40:06 1999 +0200 @@ -90,7 +90,7 @@ \ size (rel s) = k & ask s ! k <= giv s ! k}"; by (res_inst_tac [("act", "rel_act")] transient_mem 1); by (auto_tac (claset(), - simpset() addsimps [Domain_def, Acts_Join, Cli_prg_def])); + simpset() addsimps [Domain_def, Cli_prg_def])); qed "transient_lemma";