--- a/src/HOL/Multivariate_Analysis/Integration.certs Sun Dec 19 18:54:29 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.certs Sun Dec 19 18:55:21 2010 +0100
@@ -621,18 +621,18 @@
#427 := [unit-resolution #411 #426]: #395
[th-lemma arith farkas 2 1 2 3 1 1 #421 #319 #321 #414 #318 #427]: false
unsat
-f26ffd00d169b6b4684265a03d23c9e0efe94a58 57 0
+76aef63700c44d6a49155f473f80703718124469 57 0
#2 := false
#37 := 0::Real
decl f12 :: (-> S5 Real)
decl f13 :: (-> S4 S4 S5)
decl f14 :: (-> S3 S4)
+decl f4 :: S3
+#8 := f4
+#45 := (f14 f4)
decl f10 :: S3
#25 := f10
-#45 := (f14 f10)
-decl f4 :: S3
-#8 := f4
-#44 := (f14 f4)
+#44 := (f14 f10)
#46 := (f13 #44 #45)
#47 := (f12 #46)
#258 := (>= #47 0::Real)
@@ -642,11 +642,11 @@
#134 := [asserted]: #50
#266 := (or #49 #260)
#48 := (<= #47 0::Real)
-#114 := [asserted]: #48
+#133 := [asserted]: #48
#259 := (not #48)
#264 := (or #49 #259 #260)
#265 := [th-lemma arith triangle-eq]: #264
-#267 := [unit-resolution #265 #114]: #266
+#267 := [unit-resolution #265 #133]: #266
#268 := [unit-resolution #267 #134]: #260
#39 := (:var 0 S4)
#38 := (:var 1 S4)
@@ -670,8 +670,8 @@
#135 := (iff #42 #136)
#137 := [rewrite]: #135
#140 := [quant-intro #137]: #139
-#113 := [asserted]: #43
-#141 := [mp #113 #140]: #138
+#132 := [asserted]: #43
+#141 := [mp #132 #140]: #138
#167 := [mp~ #141 #166]: #138
#257 := [mp #167 #256]: #252
#261 := (not #252)