src/HOL/UNITY/Comp/Client.ML
changeset 13812 91713a1915ee
parent 13797 baefae13ad37
     1.1 --- a/src/HOL/UNITY/Comp/Client.ML	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Comp/Client.ML	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  \     (G : preserves rel & G : preserves ask & G : preserves tok &\
     1.5  \      Client : Allowed G)";
     1.6  by (auto_tac (claset(), 
     1.7 -      simpset() addsimps [ok_iff_Allowed, Client_def RS def_prg_Allowed]));  
     1.8 +    simpset() addsimps [ok_iff_Allowed, Client_def RS def_total_prg_Allowed]));
     1.9  qed "Client_ok_iff";
    1.10  AddIffs [Client_ok_iff];
    1.11  
    1.12 @@ -79,7 +79,8 @@
    1.13  qed "Join_Always_rel_le_giv";
    1.14  
    1.15  Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}";
    1.16 -by (res_inst_tac [("act", "rel_act")] transientI 1);
    1.17 +by (simp_tac (simpset() addsimps [Client_def, mk_total_program_def]) 1);
    1.18 +by (res_inst_tac [("act", "rel_act")] totalize_transientI 1);
    1.19  by (auto_tac (claset(),
    1.20  	      simpset() addsimps [Domain_def, Client_def]));
    1.21  by (blast_tac (claset() addIs [less_le_trans, prefix_length_le,