# HG changeset patch
# User chaieb
# Date 1242145969 -3600
# Node ID 527ba4a378436a60e795bff37f05acbe13299fd5
# Parent  379378d59b08e0a1493808776b82373fa7b088e3
Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library

diff -r 379378d59b08 -r 527ba4a37843 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon May 11 21:55:30 2009 -0700
+++ b/src/HOL/IsaMakefile	Tue May 12 17:32:49 2009 +0100
@@ -310,7 +310,8 @@
 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy		\
   Library/Abstract_Rat.thy \
   Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy	\
-  Library/Euclidean_Space.thy Library/Glbs.thy Library/normarith.ML \
+  Library/Euclidean_Space.thy Library/Sum_Of_Squares.thy Library/positivstellensatz.ML	\
+  Library/sum_of_squares.ML Library/Glbs.thy Library/normarith.ML \
   Library/Executable_Set.thy Library/Infinite_Set.thy			\
   Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
   Library/Bit.thy Library/Topology_Euclidean_Space.thy \
diff -r 379378d59b08 -r 527ba4a37843 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Mon May 11 21:55:30 2009 -0700
+++ b/src/HOL/Library/Library.thy	Tue May 12 17:32:49 2009 +0100
@@ -53,6 +53,7 @@
   Reflection
   RBT
   State_Monad
+  Sum_Of_Squares
   Topology_Euclidean_Space
   Univ_Poly
   While_Combinator