src/HOL/Old_Number_Theory/Int2.thy
changeset 38159 e9b4835a54ee
parent 32479 521cc9bf2958
child 41541 1fa4725c4656
     1.1 --- a/src/HOL/Old_Number_Theory/Int2.thy	Thu Aug 05 23:43:43 2010 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Int2.thy	Fri Aug 06 12:37:00 2010 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4 -(*  Title:      HOL/Quadratic_Reciprocity/Gauss.thy
     1.5 -    ID:         $Id$
     1.6 +(*  Title:      HOL/Old_Number_Theory/Int2.thy
     1.7      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
     1.8  *)
     1.9  
    1.10 @@ -9,9 +8,8 @@
    1.11  imports Finite2 WilsonRuss
    1.12  begin
    1.13  
    1.14 -definition
    1.15 -  MultInv :: "int => int => int" where
    1.16 -  "MultInv p x = x ^ nat (p - 2)"
    1.17 +definition MultInv :: "int => int => int"
    1.18 +  where "MultInv p x = x ^ nat (p - 2)"
    1.19  
    1.20  
    1.21  subsection {* Useful lemmas about dvd and powers *}