# HG changeset patch
# User haftmann
# Date 1256119339 -7200
# Node ID 6793b02a3409c02a90622c8cafcd44c24b87fa26
# Parent  5018f6a76b3fbd83b98de6086405182564804707
tuned ML import

diff -r 5018f6a76b3f -r 6793b02a3409 src/HOL/Library/Sum_Of_Squares.thy
--- a/src/HOL/Library/Sum_Of_Squares.thy	Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy	Wed Oct 21 12:02:19 2009 +0200
@@ -9,10 +9,10 @@
 theory Sum_Of_Squares
 imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *)
 uses
-  ("positivstellensatz.ML")  (* duplicate use!? -- cf. Euclidian_Space.thy *)
-  ("Sum_Of_Squares/sum_of_squares.ML")
-  ("Sum_Of_Squares/positivstellensatz_tools.ML")
-  ("Sum_Of_Squares/sos_wrapper.ML")
+  "positivstellensatz.ML"  (* duplicate use!? -- cf. Euclidian_Space.thy *)
+  "Sum_Of_Squares/sum_of_squares.ML"
+  "Sum_Of_Squares/positivstellensatz_tools.ML"
+  "Sum_Of_Squares/sos_wrapper.ML"
 begin
 
 text {*
@@ -28,13 +28,6 @@
   without calling an external prover.
 *}
 
-text {* setup sos tactic *}
-
-use "positivstellensatz.ML"
-use "Sum_Of_Squares/positivstellensatz_tools.ML"
-use "Sum_Of_Squares/sum_of_squares.ML"
-use "Sum_Of_Squares/sos_wrapper.ML"
-
 setup SOS_Wrapper.setup
 
 text {* Tests *}