src/HOL/Lambda/ListApplication.ML
changeset 6301 08245f5a436d
parent 6128 2acc5d36610c
child 8935 548901d05a0e
     1.1 --- a/src/HOL/Lambda/ListApplication.ML	Wed Mar 03 11:12:29 1999 +0100
     1.2 +++ b/src/HOL/Lambda/ListApplication.ML	Wed Mar 03 11:15:18 1999 +0100
     1.3 @@ -88,7 +88,7 @@
     1.4  Addsimps [size_apps];
     1.5  
     1.6  Goal "[| 0 < k; m <= n |] ==> m < n+k";
     1.7 -by(fast_arith_tac 1);
     1.8 +by (fast_arith_tac 1);
     1.9  val lemma = result();
    1.10  
    1.11  (* a customized induction schema for $$ *)