# HG changeset patch
# User wenzelm
# Date 1122916847 -7200
# Node ID 2ec0b8159e8e6bee0136c16f75c3db3849d5fb77
# Parent  38bb4f03a8877ec0397c5ac84ffaa8fbfa0ee81a
tuned;

diff -r 38bb4f03a887 -r 2ec0b8159e8e src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Mon Aug 01 19:20:46 2005 +0200
+++ b/src/HOL/ex/NatSum.thy	Mon Aug 01 19:20:47 2005 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/ex/NatSum.ML
+(*  Title: HOL/ex/NatSum.thy
     ID:         $Id$
     Author:     Tobias Nipkow
 *)
@@ -10,9 +10,6 @@
 text {*
   Summing natural numbers, squares, cubes, etc.
 
-  Originally demonstrated permutative rewriting, but @{thm [source]
-  add_ac} is no longer needed thanks to new simprocs.
-
   Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
   \url{http://www.research.att.com/~njas/sequences/}.
 *}
@@ -28,7 +25,7 @@
 *}
 
 lemma sum_of_odds: "(\<Sum>i=0..<n. Suc (i + i)) = n * n"
-  by (induct n, auto)
+  by (induct n) auto
 
 
 text {*
@@ -37,7 +34,7 @@
 
 lemma sum_of_odd_squares:
   "3 * (\<Sum>i=0..<n. Suc(2*i) * Suc(2*i)) = n * (4 * n * n - 1)"
-  by (induct n, auto)
+  by (induct n) auto
 
 
 text {*
@@ -47,7 +44,7 @@
 lemma sum_of_odd_cubes:
   "(\<Sum>i=0..<n. Suc (2*i) * Suc (2*i) * Suc (2*i)) =
     n * n * (2 * n * n - 1)"
-  by (induct n, auto)
+  by (induct n) auto
 
 text {*
   \medskip The sum of the first @{text n} positive integers equals
@@ -55,15 +52,15 @@
 
 lemma sum_of_naturals:
     "2 * (\<Sum>i=0..n. i) = n * Suc n"
-  by (induct n, auto)
+  by (induct n) auto
 
 lemma sum_of_squares:
     "6 * (\<Sum>i=0..n. i * i) = n * Suc n * Suc (2 * n)"
-  by (induct n, auto)
+  by (induct n) auto
 
 lemma sum_of_cubes:
     "4 * (\<Sum>i=0..n. i * i * i) = n * n * Suc n * Suc n"
-  by (induct n, auto)
+  by (induct n) auto
 
 
 text {*
@@ -87,13 +84,13 @@
   "30 * int (\<Sum>i=0..<m. i * i * i * i) =
     int m * (int m - 1) * (int(2 * m) - 1) *
     (int(3 * m * m) - int(3 * m) - 1)"
-  by (induct m, simp_all add: int_mult)
+  by (induct m) (simp_all add: int_mult)
 
 lemma of_nat_sum_of_fourth_powers:
   "30 * of_nat (\<Sum>i=0..<m. i * i * i * i) =
     of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
     (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
-  by (induct m, simp_all)
+  by (induct m) simp_all
 
 
 text {*
@@ -102,15 +99,12 @@
 *}
 
 lemma sum_of_2_powers: "(\<Sum>i=0..<n. 2^i) = 2^n - (1::nat)"
-  apply (induct n)
-   apply (auto split: nat_diff_split)
-  done
+  by (induct n) (auto split: nat_diff_split)
 
 lemma sum_of_3_powers: "2 * (\<Sum>i=0..<n. 3^i) = 3^n - (1::nat)"
-  by (induct n, auto)
+  by (induct n) auto
 
 lemma sum_of_powers: "0 < k ==> (k - 1) * (\<Sum>i=0..<n. k^i) = k^n - (1::nat)"
-  by (induct n, auto)
-
+  by (induct n) auto
 
 end
diff -r 38bb4f03a887 -r 2ec0b8159e8e src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Mon Aug 01 19:20:46 2005 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Mon Aug 01 19:20:47 2005 +0200
@@ -57,7 +57,7 @@
   structure Process = Process
   structure FileSys = FileSys
 end;
- 
+
 (*limit the printing depth*)
 fun print_depth n =
  (Meta.printDepth := n div 2;
@@ -114,13 +114,13 @@
 
 
 
-(** interrupts **)	(*Note: may get into race conditions*)
+(** interrupts **)      (*Note: may get into race conditions*)
 
 (* FIXME proper implementation available? *)
 
 exception Interrupt;
 
-fun ignore_interrupt f x = f x;           
+fun ignore_interrupt f x = f x;
 fun raise_interrupt f x = f x;
 
 
@@ -135,8 +135,7 @@
 fun execute command =
   let
     val tmp_name = FileSys.tmpName ();
-    val is = (Process.system (command ^ " > " ^ tmp_name); TextIO.openIn 
-tmp_name);
+    val is = (Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
     val result = TextIO.inputAll is;
   in
     TextIO.closeIn is;
diff -r 38bb4f03a887 -r 2ec0b8159e8e src/Pure/ML-Systems/polyml-time-limit.ML
--- a/src/Pure/ML-Systems/polyml-time-limit.ML	Mon Aug 01 19:20:46 2005 +0200
+++ b/src/Pure/ML-Systems/polyml-time-limit.ML	Mon Aug 01 19:20:47 2005 +0200
@@ -6,29 +6,32 @@
 Bounded time execution (similar to SML/NJ's TimeLimit structure) for Poly/ML.
 *)
 
-structure TimeLimit : sig
-	exception TimeOut
-	val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
-end = struct
-
-	exception TimeOut
+structure TimeLimit:
+sig
+  exception TimeOut
+  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
+end =
+struct
+  exception TimeOut
 
-	fun timeLimit t f x =
-	let
-		datatype ('a, 'b) union =
-			INL of 'a | INR of 'b
-		val result = Process.channel ()
-		fun workerThread () =
-			Process.send (result, SOME (INL (f x) handle exn => INR exn))
-		val interrupt = Process.console workerThread
-		val old_handle = Signal.signal (Posix.Signal.alrm, Signal.SIG_HANDLE
-			(fn _ => ((Process.send (result, NONE)) before (interrupt ()))))
-	in
-		Posix.Process.alarm t;
-		case Process.receive result of
-		  SOME (INL fx)  => (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); fx)
-		| SOME (INR exn) => (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); raise exn)
-		| NONE           => (Signal.signal (Posix.Signal.alrm, old_handle); raise TimeOut)
-	end
+  fun timeLimit t f x =
+    let
+      datatype ('a, 'b) union = INL of 'a | INR of 'b
+      val result = Process.channel ()
+      fun workerThread () =
+        Process.send (result, SOME (INL (f x) handle exn => INR exn))
+      val interrupt = Process.console workerThread
+      val old_handle = Signal.signal (Posix.Signal.alrm,
+        Signal.SIG_HANDLE (fn _ => (Process.send (result, NONE)) before (interrupt ())))
+    in
+      Posix.Process.alarm t;
+      case Process.receive result of
+        SOME (INL fx) =>
+          (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle); fx)
+      | SOME (INR exn) =>
+          (Posix.Process.alarm Time.zeroTime; Signal.signal (Posix.Signal.alrm, old_handle);
+           raise exn)
+      | NONE => (Signal.signal (Posix.Signal.alrm, old_handle); raise TimeOut)
+    end
 
 end;