isabelle: src/HOL/Library/Sum_of_Squares.thy@71cdb885b3bb (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
58630 71cdb885b3bb simplified "sos" method; wenzelm parents: 58418 diff changeset	6	header {* A decision procedure for universal multivariate real arithmetic
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	wenzelm
	Wed, 08 Oct 2014 11:09:17 +0200
changeset 58630	71cdb885b3bb
parent 58418	a04b242a7a01
child 58881	b9556a055632
permissions	-rw-r--r--