src/HOL/Fun.ML
changeset 1264 3eb91524b938
parent 923 ff1574a81019
child 1465 5d7a7e439cec
     1.1 --- a/src/HOL/Fun.ML	Wed Oct 04 13:01:05 1995 +0100
     1.2 +++ b/src/HOL/Fun.ML	Wed Oct 04 13:10:03 1995 +0100
     1.3 @@ -6,10 +6,12 @@
     1.4  Lemmas about functions.
     1.5  *)
     1.6  
     1.7 +simpset := HOL_ss;
     1.8 +
     1.9  goal Fun.thy "(f = g) = (!x. f(x)=g(x))";
    1.10  by (rtac iffI 1);
    1.11 -by(asm_simp_tac HOL_ss 1);
    1.12 -by(rtac ext 1 THEN asm_simp_tac HOL_ss 1);
    1.13 +by (Asm_simp_tac 1);
    1.14 +by (rtac ext 1 THEN Asm_simp_tac 1);
    1.15  qed "expand_fun_eq";
    1.16  
    1.17  val prems = goal Fun.thy
    1.18 @@ -194,7 +196,6 @@
    1.19  
    1.20  val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
    1.21  
    1.22 -val set_ss =
    1.23 -  HOL_ss addsimps mem_simps
    1.24 -         addcongs [ball_cong,bex_cong]
    1.25 -         setmksimps (mksimps mksimps_pairs);
    1.26 +simpset := !simpset addsimps mem_simps
    1.27 +                    addcongs [ball_cong,bex_cong]
    1.28 +                    setmksimps (mksimps mksimps_pairs);