src/HOL/Finite.ML
changeset 1264 3eb91524b938
parent 923 ff1574a81019
child 1465 5d7a7e439cec
     1.1 --- a/src/HOL/Finite.ML	Wed Oct 04 13:01:05 1995 +0100
     1.2 +++ b/src/HOL/Finite.ML	Wed Oct 04 13:10:03 1995 +0100
     1.3 @@ -33,13 +33,13 @@
     1.4  
     1.5  (** Simplification for Fin **)
     1.6  
     1.7 -val Fin_ss = set_ss addsimps Fin.intrs;
     1.8 +Addsimps Fin.intrs;
     1.9  
    1.10  (*The union of two finite sets is finite*)
    1.11  val major::prems = goal Finite.thy
    1.12      "[| F: Fin(A);  G: Fin(A) |] ==> F Un G : Fin(A)";
    1.13  by (rtac (major RS Fin_induct) 1);
    1.14 -by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_insert_left]))));
    1.15 +by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left]))));
    1.16  qed "Fin_UnI";
    1.17  
    1.18  (*Every subset of a finite set is finite*)
    1.19 @@ -48,18 +48,19 @@
    1.20  	    rtac mp, etac spec,
    1.21  	    rtac subs]);
    1.22  by (rtac (fin RS Fin_induct) 1);
    1.23 -by (simp_tac (Fin_ss addsimps [subset_Un_eq]) 1);
    1.24 +by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
    1.25  by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));
    1.26  by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
    1.27 -by (ALLGOALS (asm_simp_tac Fin_ss));
    1.28 +by (ALLGOALS Asm_simp_tac);
    1.29  qed "Fin_subset";
    1.30  
    1.31  (*The image of a finite set is finite*)
    1.32  val major::_ = goal Finite.thy
    1.33      "F: Fin(A) ==> h``F : Fin(h``A)";
    1.34  by (rtac (major RS Fin_induct) 1);
    1.35 -by (simp_tac Fin_ss 1);
    1.36 -by (asm_simp_tac (set_ss addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
    1.37 +by (Simp_tac 1);
    1.38 +by (asm_simp_tac
    1.39 +    (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
    1.40  qed "Fin_imageI";
    1.41  
    1.42  val major::prems = goal Finite.thy 
    1.43 @@ -70,7 +71,7 @@
    1.44  by (rtac (major RS Fin_induct) 1);
    1.45  by (rtac (Diff_insert RS ssubst) 2);
    1.46  by (ALLGOALS (asm_simp_tac
    1.47 -                (Fin_ss addsimps (prems@[Diff_subset RS Fin_subset]))));
    1.48 +                (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
    1.49  qed "Fin_empty_induct_lemma";
    1.50  
    1.51  val prems = goal Finite.thy