# HG changeset patch
# User nipkow
# Date 1120815533 -7200
# Node ID 99549528ce765a942d644bafb8c20fae73fc761b
# Parent  5c5f051aaaaa54ea3ef1731e5fcbfd214eaf6974
proof needed updating because of arith

diff -r 5c5f051aaaaa -r 99549528ce76 src/HOL/Extraction/Warshall.thy
--- a/src/HOL/Extraction/Warshall.thy	Fri Jul 08 11:38:30 2005 +0200
+++ b/src/HOL/Extraction/Warshall.thy	Fri Jul 08 11:38:53 2005 +0200
@@ -5,7 +5,9 @@
 
 header {* Warshall's algorithm *}
 
-theory Warshall imports Main begin
+theory Warshall
+imports Main
+begin
 
 text {*
   Derivation of Warshall's algorithm using program extraction,
@@ -138,14 +140,12 @@
       	proof
 	  from Cons show "list_all (\<lambda>x. x < Suc i) as" by simp
 	  from Cons show "is_path' r a as k" by simp
-	  from Cons and False show "\<not> list_all (\<lambda>x. x < i) as"
-	    by (simp, arith)
+	  from Cons and False show "\<not> list_all (\<lambda>x. x < i) as" by (simp)
       	qed
       	show ?thesis
       	proof
 	  from Cons False ys
-	  show "list_all (\<lambda>x. x < i) (a # ys) \<and> is_path' r j (a # ys) i"
-	    by (simp, arith)
+	  show "list_all (\<lambda>x. x<i) (a#ys) \<and> is_path' r j (a#ys) i" by simp
       	qed
       qed
     qed
@@ -172,14 +172,13 @@
       	proof
 	  from snoc show "list_all (\<lambda>x. x < Suc i) as" by simp
 	  from snoc show "is_path' r j as a" by simp
-	  from snoc and False show "\<not> list_all (\<lambda>x. x < i) as"
-	    by (simp, arith)
+	  from snoc and False show "\<not> list_all (\<lambda>x. x < i) as" by simp
       	qed
       	show ?thesis
       	proof
 	  from snoc False ys
 	  show "list_all (\<lambda>x. x < i) (ys @ [a]) \<and> is_path' r i (ys @ [a]) k"
-	    by (simp, arith)  
+	    by simp
       	qed
       qed
     qed
@@ -256,4 +255,3 @@
 *}
 
 end
-