src/HOL/Set.ML
changeset 4089 96fba19bcbe2
parent 4059 59c1422c9da5
child 4135 4830f1f5f6ea
     1.1 --- a/src/HOL/Set.ML	Mon Nov 03 12:12:10 1997 +0100
     1.2 +++ b/src/HOL/Set.ML	Mon Nov 03 12:13:18 1997 +0100
     1.3 @@ -83,12 +83,12 @@
     1.4  
     1.5  (*Trival rewrite rule*)
     1.6  goal Set.thy "(! x:A. P) = ((? x. x:A) --> P)";
     1.7 -by (simp_tac (!simpset addsimps [Ball_def]) 1);
     1.8 +by (simp_tac (simpset() addsimps [Ball_def]) 1);
     1.9  qed "ball_triv";
    1.10  
    1.11  (*Dual form for existentials*)
    1.12  goal Set.thy "(? x:A. P) = ((? x. x:A) & P)";
    1.13 -by (simp_tac (!simpset addsimps [Bex_def]) 1);
    1.14 +by (simp_tac (simpset() addsimps [Bex_def]) 1);
    1.15  qed "bex_triv";
    1.16  
    1.17  Addsimps [ball_triv, bex_triv];
    1.18 @@ -228,7 +228,7 @@
    1.19  
    1.20  qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}"
    1.21   (fn [prem]=>
    1.22 -  [ (blast_tac (!claset addIs [prem RS FalseE]) 1) ]);
    1.23 +  [ (blast_tac (claset() addIs [prem RS FalseE]) 1) ]);
    1.24  
    1.25  qed_goal "equals0D" Set.thy "!!a. [| A={};  a:A |] ==> P"
    1.26   (fn _ => [ (Blast_tac 1) ]);
    1.27 @@ -414,7 +414,7 @@
    1.28  (fn _ => [Blast_tac 1]);
    1.29  
    1.30  goal Set.thy "!!a b. {a}={b} ==> a=b";
    1.31 -by (blast_tac (!claset addEs [equalityE]) 1);
    1.32 +by (blast_tac (claset() addEs [equalityE]) 1);
    1.33  qed "singleton_inject";
    1.34  
    1.35  (*Redundant? But unlike insertCI, it proves the subgoal immediately!*)
    1.36 @@ -669,7 +669,7 @@
    1.37  		  expand_if_mem1, expand_if_mem2];
    1.38  
    1.39  
    1.40 -(*Each of these has ALREADY been added to !simpset above.*)
    1.41 +(*Each of these has ALREADY been added to simpset() above.*)
    1.42  val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
    1.43                   mem_Collect_eq, 
    1.44  		 UN_iff, UN1_iff, Union_iff, 
    1.45 @@ -677,12 +677,12 @@
    1.46  
    1.47  (*Not for Addsimps -- it can cause goals to blow up!*)
    1.48  goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
    1.49 -by (simp_tac (!simpset addsplits [expand_if]) 1);
    1.50 +by (simp_tac (simpset() addsplits [expand_if]) 1);
    1.51  qed "mem_if";
    1.52  
    1.53  val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
    1.54  
    1.55 -simpset := !simpset addcongs [ball_cong,bex_cong]
    1.56 +simpset_ref() := simpset() addcongs [ball_cong,bex_cong]
    1.57                      setmksimps (mksimps mksimps_pairs);
    1.58  
    1.59  Addsimps[subset_UNIV, empty_subsetI, subset_refl];