--- 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 *}