fixed theory deps;
authorwenzelm
Wed May 10 22:34:30 2000 +0200 (2000-05-10)
changeset 8856435187ffc64e
parent 8855 ef4848bb0696
child 8857 7ec405405dd7
fixed theory deps;
src/HOL/Real/Hyperreal/Filter.ML
src/HOL/Real/Hyperreal/HyperDef.ML
src/HOL/Real/Hyperreal/Zorn.ML
src/HOL/Real/PNat.ML
src/HOL/Real/PNat.thy
src/HOL/Real/PRat.thy
src/HOL/Real/ROOT.ML
src/HOL/Real/RealAbs.thy
src/HOL/Real/RealBin.thy
src/HOL/Real/RealInt.ML
src/HOL/Real/RealInt.thy
src/HOL/Real/RealOrd.ML
src/HOL/Real/RealPow.thy
     1.1 --- a/src/HOL/Real/Hyperreal/Filter.ML	Wed May 10 21:04:16 2000 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/Filter.ML	Wed May 10 22:34:30 2000 +0200
     1.3 @@ -552,5 +552,3 @@
     1.4  val FreeUltrafilter_Ex  = export FreeUltrafilter_ex;
     1.5  
     1.6  Close_locale "UFT";
     1.7 -
     1.8 -
     2.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Wed May 10 21:04:16 2000 +0200
     2.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Wed May 10 22:34:30 2000 +0200
     2.3 @@ -1857,371 +1857,3 @@
     2.4         "hypreal_of_nat n = hypreal_of_real (real_of_nat n)";
     2.5  by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1);
     2.6  qed "hypreal_of_nat_real_of_nat";
     2.7 -
     2.8 -
     2.9 -
    2.10 -
    2.11 -
    2.12 -
    2.13 -
    2.14 -
    2.15 -
    2.16 -
    2.17 -
    2.18 -
    2.19 -
    2.20 -
    2.21 -
    2.22 -
    2.23 -
    2.24 -
    2.25 -
    2.26 -
    2.27 -
    2.28 -
    2.29 -
    2.30 -
    2.31 -
    2.32 -
    2.33 -
    2.34 -
    2.35 -
    2.36 -
    2.37 -
    2.38 -
    2.39 -
    2.40 -
    2.41 -
    2.42 -
    2.43 -
    2.44 -
    2.45 -
    2.46 -
    2.47 -
    2.48 -
    2.49 -
    2.50 -
    2.51 -
    2.52 -
    2.53 -
    2.54 -
    2.55 -
    2.56 -
    2.57 -
    2.58 -
    2.59 -
    2.60 -
    2.61 -
    2.62 -
    2.63 -
    2.64 -
    2.65 -
    2.66 -
    2.67 -
    2.68 -
    2.69 -
    2.70 -
    2.71 -
    2.72 -
    2.73 -
    2.74 -
    2.75 -
    2.76 -
    2.77 -
    2.78 -
    2.79 -
    2.80 -
    2.81 -
    2.82 -
    2.83 -
    2.84 -
    2.85 -
    2.86 -
    2.87 -
    2.88 -
    2.89 -
    2.90 -
    2.91 -
    2.92 -
    2.93 -
    2.94 -
    2.95 -
    2.96 -
    2.97 -
    2.98 -
    2.99 -
   2.100 -
   2.101 -
   2.102 -
   2.103 -
   2.104 -
   2.105 -
   2.106 -
   2.107 -
   2.108 -
   2.109 -
   2.110 -
   2.111 -
   2.112 -
   2.113 -
   2.114 -
   2.115 -
   2.116 -
   2.117 -
   2.118 -
   2.119 -
   2.120 -
   2.121 -
   2.122 -
   2.123 -
   2.124 -
   2.125 -
   2.126 -
   2.127 -
   2.128 -
   2.129 -
   2.130 -
   2.131 -
   2.132 -
   2.133 -
   2.134 -
   2.135 -
   2.136 -
   2.137 -
   2.138 -
   2.139 -
   2.140 -
   2.141 -
   2.142 -
   2.143 -
   2.144 -
   2.145 -
   2.146 -
   2.147 -
   2.148 -
   2.149 -
   2.150 -
   2.151 -
   2.152 -
   2.153 -
   2.154 -
   2.155 -
   2.156 -
   2.157 -
   2.158 -
   2.159 -
   2.160 -
   2.161 -
   2.162 -
   2.163 -
   2.164 -
   2.165 -
   2.166 -
   2.167 -
   2.168 -
   2.169 -
   2.170 -
   2.171 -
   2.172 -
   2.173 -
   2.174 -
   2.175 -
   2.176 -
   2.177 -
   2.178 -
   2.179 -
   2.180 -
   2.181 -
   2.182 -
   2.183 -
   2.184 -
   2.185 -
   2.186 -
   2.187 -
   2.188 -
   2.189 -
   2.190 -
   2.191 -
   2.192 -
   2.193 -
   2.194 -
   2.195 -
   2.196 -
   2.197 -
   2.198 -
   2.199 -
   2.200 -
   2.201 -
   2.202 -
   2.203 -
   2.204 -
   2.205 -
   2.206 -
   2.207 -
   2.208 -
   2.209 -
   2.210 -
   2.211 -
   2.212 -
   2.213 -
   2.214 -
   2.215 -
   2.216 -
   2.217 -
   2.218 -
   2.219 -
   2.220 -
   2.221 -
   2.222 -
   2.223 -
   2.224 -
   2.225 -
   2.226 -
   2.227 -
   2.228 -
   2.229 -
   2.230 -
   2.231 -
   2.232 -
   2.233 -
   2.234 -
   2.235 -
   2.236 -
   2.237 -
   2.238 -
   2.239 -
   2.240 -
   2.241 -
   2.242 -
   2.243 -
   2.244 -
   2.245 -
   2.246 -
   2.247 -
   2.248 -
   2.249 -
   2.250 -
   2.251 -
   2.252 -
   2.253 -
   2.254 -
   2.255 -
   2.256 -
   2.257 -
   2.258 -
   2.259 -
   2.260 -
   2.261 -
   2.262 -
   2.263 -
   2.264 -
   2.265 -
   2.266 -
   2.267 -
   2.268 -
   2.269 -
   2.270 -
   2.271 -
   2.272 -
   2.273 -
   2.274 -
   2.275 -
   2.276 -
   2.277 -
   2.278 -
   2.279 -
   2.280 -
   2.281 -
   2.282 -
   2.283 -
   2.284 -
   2.285 -
   2.286 -
   2.287 -
   2.288 -
   2.289 -
   2.290 -
   2.291 -
   2.292 -
   2.293 -
   2.294 -
   2.295 -
   2.296 -
   2.297 -
   2.298 -
   2.299 -
   2.300 -
   2.301 -
   2.302 -
   2.303 -
   2.304 -
   2.305 -
   2.306 -
   2.307 -
   2.308 -
   2.309 -
   2.310 -
   2.311 -
   2.312 -
   2.313 -
   2.314 -
   2.315 -
   2.316 -
   2.317 -
   2.318 -
   2.319 -
   2.320 -
   2.321 -
   2.322 -
   2.323 -
   2.324 -
   2.325 -
   2.326 -
   2.327 -
   2.328 -
   2.329 -
   2.330 -
   2.331 -
   2.332 -
   2.333 -
   2.334 -
   2.335 -
   2.336 -
   2.337 -
   2.338 -
   2.339 -
   2.340 -
   2.341 -
   2.342 -
   2.343 -
   2.344 -
   2.345 -
   2.346 -
   2.347 -
   2.348 -
   2.349 -
   2.350 -
   2.351 -
   2.352 -
   2.353 -
   2.354 -
   2.355 -
   2.356 -
   2.357 -
   2.358 -
   2.359 -
   2.360 -
   2.361 -
   2.362 -
   2.363 -
   2.364 -
   2.365 -
   2.366 -
   2.367 -
   2.368 -
   2.369 -
   2.370 -
   2.371 -
   2.372 -
   2.373 -
   2.374 -
     3.1 --- a/src/HOL/Real/Hyperreal/Zorn.ML	Wed May 10 21:04:16 2000 +0200
     3.2 +++ b/src/HOL/Real/Hyperreal/Zorn.ML	Wed May 10 22:34:30 2000 +0200
     3.3 @@ -289,4 +289,3 @@
     3.4  Goal "x : Union(c) ==> EX m:c. x:m";
     3.5  by (Blast_tac 1);
     3.6  qed "mem_UnionD";
     3.7 -
     4.1 --- a/src/HOL/Real/PNat.ML	Wed May 10 21:04:16 2000 +0200
     4.2 +++ b/src/HOL/Real/PNat.ML	Wed May 10 22:34:30 2000 +0200
     4.3 @@ -226,7 +226,8 @@
     4.4  by (auto_tac (claset() addDs [(inj_on_Abs_pnat RS inj_onD)] 
     4.5    	               addSDs [add_eq_self_zero],
     4.6  	      simpset() addsimps [sum_Rep_pnat, Rep_pnat,Abs_pnat_inverse,
     4.7 -				  Rep_pnat_gt_zero RS less_not_refl2]));
     4.8 +				  Rep_pnat_gt_zero RS less_not_refl2]
     4.9 +                        delsimprocs Nat_Numeral_Simprocs.cancel_numerals));
    4.10  qed "pnat_no_add_ident";
    4.11  
    4.12  
     5.1 --- a/src/HOL/Real/PNat.thy	Wed May 10 21:04:16 2000 +0200
     5.2 +++ b/src/HOL/Real/PNat.thy	Wed May 10 22:34:30 2000 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  *) 
     5.5  
     5.6  
     5.7 -PNat = Arith +
     5.8 +PNat = Main +
     5.9  
    5.10  typedef
    5.11    pnat = "lfp(%X. {1} Un (Suc``X))"   (lfp_def)
     6.1 --- a/src/HOL/Real/PRat.thy	Wed May 10 21:04:16 2000 +0200
     6.2 +++ b/src/HOL/Real/PRat.thy	Wed May 10 22:34:30 2000 +0200
     6.3 @@ -5,7 +5,7 @@
     6.4      Description : The positive rationals
     6.5  *) 
     6.6  
     6.7 -PRat = PNat + Equiv +
     6.8 +PRat = PNat +
     6.9  
    6.10  constdefs
    6.11      ratrel   ::  "((pnat * pnat) * (pnat * pnat)) set"
     7.1 --- a/src/HOL/Real/ROOT.ML	Wed May 10 21:04:16 2000 +0200
     7.2 +++ b/src/HOL/Real/ROOT.ML	Wed May 10 22:34:30 2000 +0200
     7.3 @@ -13,7 +13,6 @@
     7.4  time_use_thy "RealDef";
     7.5  use          "simproc.ML";
     7.6  time_use_thy "Real";
     7.7 -time_use_thy "Hyperreal/Filter";
     7.8  time_use_thy "Hyperreal/HyperDef";
     7.9  
    7.10  (*FIXME: move to RealBin and eliminate all references to 0r, 1r in 
     8.1 --- a/src/HOL/Real/RealAbs.thy	Wed May 10 21:04:16 2000 +0200
     8.2 +++ b/src/HOL/Real/RealAbs.thy	Wed May 10 22:34:30 2000 +0200
     8.3 @@ -5,6 +5,6 @@
     8.4      Description : Absolute value function for the reals
     8.5  *) 
     8.6  
     8.7 -RealAbs = RealOrd + RealBin +
     8.8 +RealAbs = RealBin +
     8.9  
    8.10  end
     9.1 --- a/src/HOL/Real/RealBin.thy	Wed May 10 21:04:16 2000 +0200
     9.2 +++ b/src/HOL/Real/RealBin.thy	Wed May 10 22:34:30 2000 +0200
     9.3 @@ -8,7 +8,7 @@
     9.4  This case is reduced to that for the integers
     9.5  *)
     9.6  
     9.7 -RealBin = RealInt + IntArith + 
     9.8 +RealBin = RealInt +
     9.9  
    9.10  instance
    9.11    real :: number 
    10.1 --- a/src/HOL/Real/RealInt.ML	Wed May 10 21:04:16 2000 +0200
    10.2 +++ b/src/HOL/Real/RealInt.ML	Wed May 10 22:34:30 2000 +0200
    10.3 @@ -80,14 +80,15 @@
    10.4  
    10.5  Goal "real_of_int (int (Suc n)) = real_of_int (int n) + 1r";
    10.6  by (simp_tac (simpset() addsimps [real_of_int_one RS sym,
    10.7 -				  real_of_int_add,zadd_int]) 1);
    10.8 +				  real_of_int_add,zadd_int] @ zadd_ac) 1);
    10.9  qed "real_of_int_Suc";
   10.10  
   10.11  (* relating two of the embeddings *)
   10.12  Goal "real_of_int (int n) = real_of_nat n";
   10.13  by (induct_tac "n" 1);
   10.14 -by (auto_tac (claset(),simpset() addsimps [real_of_int_zero,
   10.15 -    real_of_nat_zero,real_of_int_Suc,real_of_nat_Suc]));
   10.16 +by (ALLGOALS (simp_tac (HOL_ss addsimps [real_of_int_zero,
   10.17 +    real_of_nat_zero,real_of_int_Suc,real_of_nat_Suc])));
   10.18 +by (Simp_tac 1);
   10.19  qed "real_of_int_real_of_nat";
   10.20  
   10.21  Goal "~neg z ==> real_of_nat (nat z) = real_of_int z";
   10.22 @@ -104,7 +105,7 @@
   10.23  
   10.24  Goal "(real_of_int x = 0r) = (x = int 0)";
   10.25  by (auto_tac (claset() addIs [inj_real_of_int RS injD],
   10.26 -    simpset() addsimps [real_of_int_zero]));
   10.27 +    HOL_ss addsimps [real_of_int_zero]));
   10.28  qed "real_of_int_zero_cancel";
   10.29  Addsimps [real_of_int_zero_cancel];
   10.30  
   10.31 @@ -118,7 +119,7 @@
   10.32  
   10.33  Goal "x < y ==> (real_of_int x < real_of_int y)";
   10.34  by (auto_tac (claset(),
   10.35 -	      simpset() addsimps [zless_iff_Suc_zadd, real_of_int_add RS sym,
   10.36 +	      HOL_ss addsimps [zless_iff_Suc_zadd, real_of_int_add RS sym,
   10.37  				  real_of_int_real_of_nat,
   10.38  				  real_of_nat_Suc]));
   10.39  by (simp_tac (simpset() addsimps [real_of_nat_one RS
    11.1 --- a/src/HOL/Real/RealInt.thy	Wed May 10 21:04:16 2000 +0200
    11.2 +++ b/src/HOL/Real/RealInt.thy	Wed May 10 22:34:30 2000 +0200
    11.3 @@ -5,7 +5,7 @@
    11.4      Description: Embedding the integers in the reals
    11.5  *)
    11.6  
    11.7 -RealInt = RealOrd + Int + 
    11.8 +RealInt = RealOrd +
    11.9  
   11.10  constdefs 
   11.11     real_of_int :: int => real
    12.1 --- a/src/HOL/Real/RealOrd.ML	Wed May 10 21:04:16 2000 +0200
    12.2 +++ b/src/HOL/Real/RealOrd.ML	Wed May 10 22:34:30 2000 +0200
    12.3 @@ -812,7 +812,8 @@
    12.4  by (dtac lemma_nat_not_dense 1);
    12.5  by (auto_tac (claset(),
    12.6  	      simpset() addsimps [real_of_nat_Suc, real_of_nat_zero] @ 
    12.7 -	                         real_add_ac));
    12.8 +	                         real_add_ac
    12.9 +                        delsimprocs Nat_Numeral_Simprocs.cancel_numerals));
   12.10  by (asm_full_simp_tac (simpset() addsimps [real_of_nat_one RS sym,
   12.11  					   real_of_nat_add,Suc_diff_n]) 1);
   12.12  qed "real_of_nat_minus";
    13.1 --- a/src/HOL/Real/RealPow.thy	Wed May 10 21:04:16 2000 +0200
    13.2 +++ b/src/HOL/Real/RealPow.thy	Wed May 10 22:34:30 2000 +0200
    13.3 @@ -6,11 +6,11 @@
    13.4  
    13.5  *)
    13.6  
    13.7 -RealPow = WF_Rel + RealAbs + 
    13.8 +RealPow = RealAbs +
    13.9  
   13.10  instance real :: {power}
   13.11  
   13.12 -primrec
   13.13 +primrec (realpow)
   13.14       realpow_0   "r ^ 0       = 1r"
   13.15       realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)"
   13.16