# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1391386968 0
# Node ID 16724746ad89dd04b455f5f5e178470a0f83b618
# Parent  ad3604df6bc6607a648df5efbd9ac4b80cf29ca0
fixed indentation

diff -r ad3604df6bc6 -r 16724746ad89 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Sun Feb 02 21:48:28 2014 +0000
+++ b/src/HOL/Number_Theory/Residues.thy	Mon Feb 03 00:22:48 2014 +0000
@@ -312,9 +312,9 @@
       done
     with `x dvd p` `1 < x` have "False" by auto }
   then show ?thesis 
-    using `2 \<le> p` apply (simp add: prime_def)
-by (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 
-  not_numeral_le_zero one_dvd)
+    using `2 \<le> p` 
+    by (simp add: prime_def)
+       (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 not_numeral_le_zero one_dvd)
 qed
 
 lemma phi_zero [simp]: "phi 0 = 0"