src/Tools/isac/Knowledge/Test.thy
branchisac-update-Isa09-2
changeset 37971 62ad72be5632
parent 37969 81922154e742
child 37972 66fc615a1e89
equal deleted inserted replaced
37970:6df5d02e46ba 37971:62ad72be5632
  1217 val scr_make_polytest = 
  1217 val scr_make_polytest = 
  1218 "Script Expand_binomtest t_ =" ^
  1218 "Script Expand_binomtest t_ =" ^
  1219 "(Repeat                       " ^
  1219 "(Repeat                       " ^
  1220 "((Try (Repeat (Rewrite real_diff_minus         False))) @@ " ^ 
  1220 "((Try (Repeat (Rewrite real_diff_minus         False))) @@ " ^ 
  1221 
  1221 
  1222 " (Try (Repeat (Rewrite real_add_mult_distrib   False))) @@ " ^	 
  1222 " (Try (Repeat (Rewrite left_distrib   False))) @@ " ^	 
  1223 " (Try (Repeat (Rewrite real_add_mult_distrib2  False))) @@ " ^	
  1223 " (Try (Repeat (Rewrite right_distrib  False))) @@ " ^	
  1224 " (Try (Repeat (Rewrite real_diff_mult_distrib  False))) @@ " ^	
  1224 " (Try (Repeat (Rewrite left_diff_distrib  False))) @@ " ^	
  1225 " (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ " ^	
  1225 " (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^	
  1226 
  1226 
  1227 " (Try (Repeat (Rewrite real_mult_1             False))) @@ " ^		   
  1227 " (Try (Repeat (Rewrite mult_1_left             False))) @@ " ^		   
  1228 " (Try (Repeat (Rewrite real_mult_0             False))) @@ " ^		   
  1228 " (Try (Repeat (Rewrite mult_zero_left             False))) @@ " ^		   
  1229 " (Try (Repeat (Rewrite real_add_zero_left      False))) @@ " ^	 
  1229 " (Try (Repeat (Rewrite add_0_left      False))) @@ " ^	 
  1230 
  1230 
  1231 " (Try (Repeat (Rewrite real_mult_commute       False))) @@ " ^		
  1231 " (Try (Repeat (Rewrite real_mult_commute       False))) @@ " ^		
  1232 " (Try (Repeat (Rewrite real_mult_left_commute  False))) @@ " ^	
  1232 " (Try (Repeat (Rewrite real_mult_left_commute  False))) @@ " ^	
  1233 " (Try (Repeat (Rewrite real_mult_assoc         False))) @@ " ^		
  1233 " (Try (Repeat (Rewrite real_mult_assoc         False))) @@ " ^		
  1234 " (Try (Repeat (Rewrite real_add_commute        False))) @@ " ^		
  1234 " (Try (Repeat (Rewrite add_commute        False))) @@ " ^		
  1235 " (Try (Repeat (Rewrite real_add_left_commute   False))) @@ " ^	 
  1235 " (Try (Repeat (Rewrite add_left_commute   False))) @@ " ^	 
  1236 " (Try (Repeat (Rewrite real_add_assoc          False))) @@ " ^	 
  1236 " (Try (Repeat (Rewrite add_assoc          False))) @@ " ^	 
  1237 
  1237 
  1238 " (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ " ^	 
  1238 " (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ " ^	 
  1239 " (Try (Repeat (Rewrite realpow_plus_1          False))) @@ " ^	 
  1239 " (Try (Repeat (Rewrite realpow_plus_1          False))) @@ " ^	 
  1240 " (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ " ^		
  1240 " (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ " ^		
  1241 " (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ " ^		
  1241 " (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ " ^		
  1329 " (Try (Repeat (Rewrite real_minus_binom_pow2   False))) @@ " ^
  1329 " (Try (Repeat (Rewrite real_minus_binom_pow2   False))) @@ " ^
  1330 " (Try (Repeat (Rewrite real_minus_binom_times  False))) @@ " ^
  1330 " (Try (Repeat (Rewrite real_minus_binom_times  False))) @@ " ^
  1331 " (Try (Repeat (Rewrite real_plus_minus_binom1  False))) @@ " ^
  1331 " (Try (Repeat (Rewrite real_plus_minus_binom1  False))) @@ " ^
  1332 " (Try (Repeat (Rewrite real_plus_minus_binom2  False))) @@ " ^
  1332 " (Try (Repeat (Rewrite real_plus_minus_binom2  False))) @@ " ^
  1333 
  1333 
  1334 " (Try (Repeat (Rewrite real_mult_1             False))) @@ " ^
  1334 " (Try (Repeat (Rewrite mult_1_left             False))) @@ " ^
  1335 " (Try (Repeat (Rewrite real_mult_0             False))) @@ " ^
  1335 " (Try (Repeat (Rewrite mult_zero_left             False))) @@ " ^
  1336 " (Try (Repeat (Rewrite real_add_zero_left      False))) @@ " ^
  1336 " (Try (Repeat (Rewrite add_0_left      False))) @@ " ^
  1337 
  1337 
  1338 " (Try (Repeat (Calculate plus  ))) @@ " ^
  1338 " (Try (Repeat (Calculate plus  ))) @@ " ^
  1339 " (Try (Repeat (Calculate times ))) @@ " ^
  1339 " (Try (Repeat (Calculate times ))) @@ " ^
  1340 " (Try (Repeat (Calculate power_))) @@ " ^
  1340 " (Try (Repeat (Calculate power_))) @@ " ^
  1341 
  1341