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