src/Pure/library.ML
changeset 245 faf3de36fdb1
parent 233 efd6b4bb14dd
child 255 ee132db91681
equal deleted inserted replaced
244:929fc2c63bd0 245:faf3de36fdb1
   284 
   284 
   285 (** integers **)
   285 (** integers **)
   286 
   286 
   287 fun inc i = i := ! i + 1;
   287 fun inc i = i := ! i + 1;
   288 fun dec i = i := ! i - 1;
   288 fun dec i = i := ! i - 1;
   289 
       
   290 
       
   291 fun square (n:int) = n * n;
       
   292 
       
   293 fun fact 0 = 1
       
   294   | fact n = n * fact (n - 1);
       
   295 
   289 
   296 
   290 
   297 (* lists of integers *)
   291 (* lists of integers *)
   298 
   292 
   299 (*make the list [from, from + 1, ..., to]*)
   293 (*make the list [from, from + 1, ..., to]*)