src/HOL/Integ/Integ.ML
changeset 4477 b3e5857d8d99
parent 4473 803d1e302af1
child 4676 335dfafb1816
     1.1 --- a/src/HOL/Integ/Integ.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/Integ/Integ.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -847,7 +847,7 @@
     1.4  	  negative_eq_positive, not_znat_zless_negative]; 
     1.5  
     1.6  goalw Integ.thy [zdiff_def,zless_def] "!! x. znegative x = (x < $# 0)";
     1.7 -  by (Auto_tac()); 
     1.8 +  by Auto_tac; 
     1.9  qed "znegative_less_0"; 
    1.10  
    1.11  goalw Integ.thy [zdiff_def,zless_def] "!! x. (~znegative x) = ($# 0 <= x)";
    1.12 @@ -868,7 +868,7 @@
    1.13    by (dtac zle_imp_zless_or_eq 1); 
    1.14    by (etac disjE 1); 
    1.15    by (dtac zless_eq_zadd_Suc 1); 
    1.16 -  by (Auto_tac()); 
    1.17 +  by Auto_tac; 
    1.18  qed "not_znegativeD"; 
    1.19  
    1.20  (* a case theorem distinguishing positive and negative int *)