isabelle: src/HOL/Library/Sum_of_Squares.thy@fb544855e3b1 (annotated)

41474 60d091240485 renamed Sum_Of_Squares to Sum_of_Squares; wenzelm parents: 38805 diff changeset	1	(* Title: HOL/Library/Sum_of_Squares.thy
32949 aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref; wenzelm parents: 32645 diff changeset	2	Author: Amine Chaieb, University of Cambridge
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref; wenzelm parents: 32645 diff changeset	3	Author: Philipp Meyer, TU Muenchen
31119 2532bb2d65c7 A decision method for universal multivariate real arithmetic with add chaieb parents: diff changeset	4	*)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add chaieb parents: diff changeset	5
58881 b9556a055632 modernized header; wenzelm parents: 58630 diff changeset	6	section {* A decision procedure for universal multivariate real arithmetic
58630 71cdb885b3bb simplified "sos" method; wenzelm parents: 58418 diff changeset	7	with addition, multiplication and ordering using semidefinite programming *}
32271 378ebd64447d sos comments modified nipkow parents: 32268 diff changeset	8
41474 60d091240485 renamed Sum_Of_Squares to Sum_of_Squares; wenzelm parents: 38805 diff changeset	9	theory Sum_of_Squares
38136 bd4965bb7bdc tuned headers -- more precise load path; wenzelm parents: 33041 diff changeset	10	imports Complex_Main
32332 bc5cec7b2be6 misc changes to SOS by Philipp Meyer: wenzelm parents: 32271 diff changeset	11	begin
31119 2532bb2d65c7 A decision method for universal multivariate real arithmetic with add chaieb parents: diff changeset	12
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46593 diff changeset	13	ML_file "positivstellensatz.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46593 diff changeset	14	ML_file "Sum_of_Squares/sum_of_squares.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46593 diff changeset	15	ML_file "Sum_of_Squares/positivstellensatz_tools.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46593 diff changeset	16	ML_file "Sum_of_Squares/sos_wrapper.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46593 diff changeset	17
31119 2532bb2d65c7 A decision method for universal multivariate real arithmetic with add chaieb parents: diff changeset	18	end

author	blanchet
	Tue, 10 Mar 2015 09:49:17 +0100
changeset 59663	fb544855e3b1
parent 58881	b9556a055632
child 60500	903bb1495239
permissions	-rw-r--r--