diff -r 8aaa21db41f3 -r e9b4835a54ee src/HOL/Old_Number_Theory/Euler.thy
--- a/src/HOL/Old_Number_Theory/Euler.thy	Thu Aug 05 23:43:43 2010 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy	Fri Aug 06 12:37:00 2010 +0200
@@ -1,19 +1,18 @@
-(*  Title:      HOL/Quadratic_Reciprocity/Euler.thy
-    ID:         $Id$
+(*  Title:      HOL/Old_Number_Theory/Euler.thy
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 *)
 
 header {* Euler's criterion *}
 
-theory Euler imports Residues EvenOdd begin
+theory Euler
+imports Residues EvenOdd
+begin
 
-definition
-  MultInvPair :: "int => int => int => int set" where
-  "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
+definition MultInvPair :: "int => int => int => int set"
+  where "MultInvPair a p j = {StandardRes p j, StandardRes p (a * (MultInv p j))}"
 
-definition
-  SetS        :: "int => int => int set set" where
-  "SetS        a p   =  (MultInvPair a p ` SRStar p)"
+definition SetS :: "int => int => int set set"
+  where "SetS a p = MultInvPair a p ` SRStar p"
 
 
 subsection {* Property for MultInvPair *}