src/HOL/Set.ML
changeset 9108 9fff97d29837
parent 9088 453996655ac2
child 9161 cee6d5aee7c8
     1.1 --- a/src/HOL/Set.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Set.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  by (rtac (prem RS ext RS arg_cong) 1);
     1.5  qed "Collect_cong";
     1.6  
     1.7 -val CollectE = make_elim CollectD;
     1.8 +bind_thm ("CollectE", make_elim CollectD);
     1.9  
    1.10  AddSIs [CollectI];
    1.11  AddSEs [CollectE];
    1.12 @@ -191,7 +191,7 @@
    1.13  by (rtac set_ext 1);
    1.14  by (blast_tac (claset() addIs [subsetD]) 1);
    1.15  qed "subset_antisym";
    1.16 -val equalityI = subset_antisym;
    1.17 +bind_thm ("equalityI", subset_antisym);
    1.18  
    1.19  AddSIs [equalityI];
    1.20  
    1.21 @@ -325,8 +325,8 @@
    1.22  qed "PowD";
    1.23  
    1.24  
    1.25 -val Pow_bottom = empty_subsetI RS PowI;        (* {}: Pow(B) *)
    1.26 -val Pow_top = subset_refl RS PowI;             (* A : Pow(A) *)
    1.27 +bind_thm ("Pow_bottom", empty_subsetI RS PowI);        (* {}: Pow(B) *)
    1.28 +bind_thm ("Pow_top", subset_refl RS PowI);             (* A : Pow(A) *)
    1.29  
    1.30  
    1.31  section "Set complement";
    1.32 @@ -348,7 +348,7 @@
    1.33  by (etac CollectD 1);
    1.34  qed "ComplD";
    1.35  
    1.36 -val ComplE = make_elim ComplD;
    1.37 +bind_thm ("ComplE", make_elim ComplD);
    1.38  
    1.39  AddSIs [ComplI];
    1.40  AddSEs [ComplE];
    1.41 @@ -720,13 +720,13 @@
    1.42  bind_thm ("split_if_mem2", 
    1.43      read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
    1.44  
    1.45 -val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2,
    1.46 -		  split_if_mem1, split_if_mem2];
    1.47 +bind_thms ("split_ifs", [if_bool_eq_conj, split_if_eq1, split_if_eq2,
    1.48 +		  split_if_mem1, split_if_mem2]);
    1.49  
    1.50  
    1.51  (*Each of these has ALREADY been added to simpset() above.*)
    1.52 -val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
    1.53 -                 mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff];
    1.54 +bind_thms ("mem_simps", [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
    1.55 +                 mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff]);
    1.56  
    1.57  (*Would like to add these, but the existing code only searches for the 
    1.58    outer-level constant, which in this case is just "op :"; we instead need