# HG changeset patch
# User huffman
# Date 1329928433 -3600
# Node ID c96bd702d1dd2f2b6ef66b71e5eecfc935304f3a
# Parent  4895d7f1be4297393389c94dfa61cc6887b7f022
tuned whitespace

diff -r 4895d7f1be42 -r c96bd702d1dd src/HOL/Library/Sum_of_Squares.thy
--- a/src/HOL/Library/Sum_of_Squares.thy	Wed Feb 22 12:30:01 2012 +0100
+++ b/src/HOL/Library/Sum_of_Squares.thy	Wed Feb 22 17:33:53 2012 +0100
@@ -165,4 +165,3 @@
 by (sos_cert "((((((A<0 * A<1) * R<1) + ([~4] * A=0))) & ((((A<0 * A<1) * R<1) + ([4] * A=0)))) & (((((A<0 * A<1) * R<1) + ([4] * A=0))) & ((((A<0 * A<1) * R<1) + ([~4] * A=0)))))")
 
 end
-