--- a/src/HOL/NumberTheory/Gauss.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/NumberTheory/Gauss.thy Fri Nov 17 02:20:03 2006 +0100
@@ -18,22 +18,27 @@
begin
definition
- A :: "int set"
+ A :: "int set" where
"A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
- B :: "int set"
+definition
+ B :: "int set" where
"B = (%x. x * a) ` A"
- C :: "int set"
+definition
+ C :: "int set" where
"C = StandardRes p ` B"
- D :: "int set"
+definition
+ D :: "int set" where
"D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
- E :: "int set"
+definition
+ E :: "int set" where
"E = C \<inter> {x. ((p - 1) div 2) < x}"
- F :: "int set"
+definition
+ F :: "int set" where
"F = (%x. (p - x)) ` E"