1.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Wed Jun 14 18:23:51 2000 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Wed Jun 14 18:24:41 2000 +0200
     1.3 @@ -347,8 +347,9 @@
     1.4  by (rotate_tac 1 1);
     1.5  by (asm_full_simp_tac (simpset() addsimps 
     1.6      [hypreal_hrinv,hypreal_zero_def] setloop (split_tac [expand_if])) 1);
     1.7 -by (ultra_tac (claset() addDs (map (full_rename_numerals thy)
     1.8 -    [rinv_not_zero,real_rinv_rinv]),simpset()) 1);
     1.9 +by (ultra_tac (claset() addDs (map (rename_numerals thy)
    1.10 +			       [rinv_not_zero,real_rinv_rinv]),
    1.11 +	       simpset()) 1);
    1.12  qed "hypreal_hrinv_hrinv";
    1.13  
    1.14  Addsimps [hypreal_hrinv_hrinv];
    1.15 @@ -713,8 +714,9 @@
    1.16  by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv,
    1.17      hypreal_mult] setloop (split_tac [expand_if])) 1);
    1.18  by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
    1.19 -by (ultra_tac (claset() addIs [ccontr] addDs 
    1.20 -    [full_rename_numerals thy rinv_not_zero],simpset()) 1);
    1.21 +by (ultra_tac (claset() addIs [ccontr]
    1.22 +                        addDs [rename_numerals thy rinv_not_zero],
    1.23 +	       simpset()) 1);
    1.24  qed "hrinv_not_zero";
    1.25  
    1.26  Addsimps [hypreal_mult_hrinv,hypreal_mult_hrinv_left];
    1.27 @@ -858,8 +860,8 @@
    1.28  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
    1.29  by (auto_tac (claset() addSIs [exI],simpset() addsimps
    1.30      [hypreal_less_def,hypreal_mult]));
    1.31 -by (ultra_tac (claset() addIs [rename_numerals thy 
    1.32 -    real_mult_order],simpset()) 1);
    1.33 +by (ultra_tac (claset() addIs [rename_numerals thy real_mult_order],
    1.34 +	       simpset()) 1);
    1.35  qed "hypreal_mult_order";
    1.36  
    1.37  (*---------------------------------------------------------------------------------
    1.38 @@ -1269,14 +1271,14 @@
    1.39    hypreal_of_real preserves field and order properties
    1.40   -----------------------------------------------------------*)
    1.41  Goalw [hypreal_of_real_def] 
    1.42 -      "hypreal_of_real ((z1::real) + z2) = \
    1.43 -\      hypreal_of_real z1 + hypreal_of_real z2";
    1.44 +     "hypreal_of_real (z1 + z2) = \
    1.45 +\     hypreal_of_real z1 + hypreal_of_real z2";
    1.46  by (asm_simp_tac (simpset() addsimps [hypreal_add,
    1.47         hypreal_add_mult_distrib]) 1);
    1.48  qed "hypreal_of_real_add";
    1.49  
    1.50  Goalw [hypreal_of_real_def] 
    1.51 -            "hypreal_of_real ((z1::real) * z2) = hypreal_of_real z1 * hypreal_of_real z2";
    1.52 +     "hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2";
    1.53  by (full_simp_tac (simpset() addsimps [hypreal_mult,
    1.54          hypreal_add_mult_distrib2]) 1);
    1.55  qed "hypreal_of_real_mult";
    1.56 @@ -1674,9 +1676,9 @@
    1.57  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    1.58  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
    1.59  by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
    1.60 -by (auto_tac (claset(),simpset() addsimps 
    1.61 -    [hypreal_mult,hypreal_add,hypreal_le,
    1.62 -    rename_numerals thy real_le_add_order]));
    1.63 +by (auto_tac (claset(),
    1.64 +	      simpset() addsimps [hypreal_mult, hypreal_add, hypreal_le,
    1.65 +				  rename_numerals thy real_le_add_order]));
    1.66  qed "hypreal_self_le_add_pos2";
    1.67  Addsimps [hypreal_self_le_add_pos2];
    1.68  
    1.69 @@ -1691,11 +1693,13 @@
    1.70  qed "hypreal_of_posnat_one";
    1.71  
    1.72  Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
    1.73 -by (full_simp_tac (simpset() addsimps [real_of_preal_def,
    1.74 -    rename_numerals thy (real_one_def RS meta_eq_to_obj_eq),
    1.75 -     hypreal_add,hypreal_of_real_def,pnat_two_eq,hypreal_one_def,
    1.76 -    real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym] @ 
    1.77 -    pnat_add_ac) 1);
    1.78 +by (full_simp_tac (simpset() addsimps 
    1.79 +		   [real_of_preal_def,
    1.80 +		    rename_numerals thy (real_one_def RS meta_eq_to_obj_eq),
    1.81 +		    hypreal_add,hypreal_of_real_def,pnat_two_eq,
    1.82 +		    hypreal_one_def, real_add,
    1.83 +		    prat_of_pnat_add RS sym, preal_of_prat_add RS sym] @ 
    1.84 +		    pnat_add_ac) 1);
    1.85  qed "hypreal_of_posnat_two";
    1.86  
    1.87  Goalw [hypreal_of_posnat_def]
    1.88 @@ -1786,8 +1790,8 @@
    1.89  qed "hypreal_of_real_not_eq_epsilon";
    1.90  
    1.91  Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0";
    1.92 -by (auto_tac (claset(),simpset() addsimps 
    1.93 -    [rename_numerals thy real_of_posnat_rinv_not_zero]));
    1.94 +by (auto_tac (claset(),
    1.95 +     simpset() addsimps [rename_numerals thy real_of_posnat_rinv_not_zero]));
    1.96  qed "hypreal_epsilon_not_zero";
    1.97  
    1.98  Addsimps [rename_numerals thy real_of_posnat_not_eq_zero];