src/HOL/UNITY/Follows.ML
changeset 10265 4e004b548049
parent 9104 89ca2a172f84
child 11786 51ce34ef5113
     1.1 --- a/src/HOL/UNITY/Follows.ML	Wed Oct 18 23:41:28 2000 +0200
     1.2 +++ b/src/HOL/UNITY/Follows.ML	Wed Oct 18 23:42:18 2000 +0200
     1.3 @@ -180,7 +180,7 @@
     1.4  by (dres_inst_tac [("x","f xa")] spec 1);
     1.5  by (dres_inst_tac [("x","g xa")] spec 1);
     1.6  by (ball_tac 1);
     1.7 -by (blast_tac (claset() addIs [union_le_mono, order_trans]) 1); 
     1.8 +by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1); 
     1.9  qed "increasing_union";
    1.10  
    1.11  Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
    1.12 @@ -190,13 +190,13 @@
    1.13  by (dres_inst_tac [("x","f xa")] spec 1);
    1.14  by (dres_inst_tac [("x","g xa")] spec 1);
    1.15  by (ball_tac 1);
    1.16 -by (blast_tac (claset()  addIs [union_le_mono, order_trans]) 1);
    1.17 +by (blast_tac (claset()  addIs [thm "union_le_mono", order_trans]) 1);
    1.18  qed "Increasing_union";
    1.19  
    1.20  Goal "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] \
    1.21  \     ==> F : Always {s. f' s + g' s <= f s + (g s :: ('a::order) multiset)}";
    1.22  by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
    1.23 -by (blast_tac (claset()  addIs [union_le_mono]) 1);
    1.24 +by (blast_tac (claset()  addIs [thm "union_le_mono"]) 1);
    1.25  qed "Always_union";
    1.26  
    1.27  (*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
    1.28 @@ -214,7 +214,7 @@
    1.29  by (etac Stable_Int 1);
    1.30  by (assume_tac 1);
    1.31  by (Blast_tac 1);
    1.32 -by (blast_tac (claset() addIs [union_le_mono, order_trans]) 1); 
    1.33 +by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1); 
    1.34  qed "Follows_union_lemma";
    1.35  
    1.36  (*The !! is there to influence to effect of permutative rewriting at the end*)
    1.37 @@ -227,7 +227,7 @@
    1.38  by (rtac LeadsTo_Trans 1);
    1.39  by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
    1.40  (*now exchange union's arguments*)
    1.41 -by (simp_tac (simpset() addsimps [union_commute]) 1); 
    1.42 +by (simp_tac (simpset() addsimps [thm "union_commute"]) 1); 
    1.43  by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
    1.44  qed "Follows_union";
    1.45