isabelle: src/HOL/Library/Sum_of_Squares.thy@0263787a06b4 (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
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 58881 diff changeset	6	section \<open>A decision procedure for universal multivariate real arithmetic
903bb1495239 isabelle update_cartouches; wenzelm parents: 58881 diff changeset	7	with addition, multiplication and ordering using semidefinite programming\<close>
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
70333 0f7edf0853df tuned file system structure haftmann parents: 69605 diff changeset	13	ML_file \<open>Sum_of_Squares/positivstellensatz.ML\<close>
0f7edf0853df tuned file system structure haftmann parents: 69605 diff changeset	14	ML_file \<open>Sum_of_Squares/positivstellensatz_tools.ML\<close>
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 60500 diff changeset	15	ML_file \<open>Sum_of_Squares/sum_of_squares.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 60500 diff changeset	16	ML_file \<open>Sum_of_Squares/sos_wrapper.ML\<close>
48891 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	paulson <lp15@cam.ac.uk>
	Sat, 04 Dec 2021 20:30:16 +0000
changeset 74878	0263787a06b4
parent 70333	0f7edf0853df
permissions	-rw-r--r--