src/HOL/UNITY/Client.ML
changeset 7826 c6a8b73b6c2a
parent 7594 8a188ef6545e
child 7878 43b03d412b82
     1.1 --- a/src/HOL/UNITY/Client.ML	Mon Oct 11 10:52:51 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Client.ML	Mon Oct 11 10:53:39 1999 +0200
     1.3 @@ -114,6 +114,7 @@
     1.4  by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
     1.5  	               addIs [Increasing_localTo_Stable, 
     1.6  			      stable_size_rel_le_giv]) 2);
     1.7 +by (full_simp_tac (simpset() addsimps [Join_localTo]) 1);
     1.8  by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
     1.9  	               addIs [stable_localTo_stable2 RS stable_imp_Stable,
    1.10  			      stable_size_ask_le_rel]) 1);
    1.11 @@ -133,7 +134,7 @@
    1.12  	       simpset()) 1);
    1.13  by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
    1.14  by (Blast_tac 1);
    1.15 -by (auto_tac (claset(), 
    1.16 -	      simpset() addsimps [Always_eq_includes_reachable, giv_meets_ask_def]));
    1.17 -by (ALLGOALS Force_tac);
    1.18 +by (force_tac (claset(), 
    1.19 +	       simpset() addsimps [Always_eq_includes_reachable, 
    1.20 +				  giv_meets_ask_def]) 1);
    1.21  qed "client_correct";