# HG changeset patch
# User nipkow
# Date 1179556995 -7200
# Node ID 00d8bf2fce42874c62d8a0c5cdc798160fd27660
# Parent  c38c9039dc138ff44d79b91de36b205fe2aac336
Had to replace "case 1/2" by "case base/step". No idea why.

diff -r c38c9039dc13 -r 00d8bf2fce42 src/HOL/Library/Graphs.thy
--- a/src/HOL/Library/Graphs.thy	Sat May 19 07:47:51 2007 +0200
+++ b/src/HOL/Library/Graphs.thy	Sat May 19 08:43:15 2007 +0200
@@ -488,9 +488,9 @@
   shows "has_fpath G (p\<langle>i,j\<rangle>)"
   using l
 proof (induct i rule:inc_induct)
-  case 1 show ?case by (auto simp:sub_path_def intro:has_fpath.intros)
+  case base show ?case by (auto simp:sub_path_def intro:has_fpath.intros)
 next
-  case (2 i)
+  case (step i)
   with ipath upt_rec[of i j]
   show ?case
     by (auto simp:sub_path_def has_ipath_def intro:has_fpath.intros)
diff -r c38c9039dc13 -r 00d8bf2fce42 src/HOL/Library/SCT_Theorem.thy
--- a/src/HOL/Library/SCT_Theorem.thy	Sat May 19 07:47:51 2007 +0200
+++ b/src/HOL/Library/SCT_Theorem.thy	Sat May 19 08:43:15 2007 +0200
@@ -592,17 +592,13 @@
 
 
 lemma Lemma7a:
-assumes "i \<le> j"
-shows
-  "has_fth p i j m n = 
-  eql (prod (p\<langle>i,j\<rangle>)) m n"
-using prems
+ "i \<le> j \<Longrightarrow> has_fth p i j m n = eql (prod (p\<langle>i,j\<rangle>)) m n"
 proof (induct i arbitrary: m rule:inc_induct)
-  case 1 show ?case
+  case base show ?case
     unfolding has_fth_def is_fthread_def sub_path_def
     by (auto simp:in_grunit one_sedge_def)
 next
-  case (2 i)
+  case (step i)
   note IH = `\<And>m. has_fth p (Suc i) j m n = 
   eql (prod (p\<langle>Suc i,j\<rangle>)) m n`
 
@@ -630,11 +626,11 @@
   dsc (prod (p\<langle>i,j\<rangle>)) m n"
 using prems
 proof (induct i arbitrary: m rule:inc_induct)
-  case 1 show ?case
+  case base show ?case
     unfolding has_desc_fth_def is_desc_fthread_def sub_path_def 
     by (auto simp:in_grunit one_sedge_def)
 next
-  case (2 i)
+  case (step i)
   thus ?case 
     by (simp only:prod_unfold desc_scgcomp desc_fth_single
     has_dfth_unfold fth_single Lemma7a) auto
@@ -1268,9 +1264,9 @@
     from `i < j` `j < k` have "i < k" by auto
     hence "prod (?cp\<langle>i, k\<rangle>) = G"
     proof (induct i rule:strict_inc_induct)
-      case 1 thus ?case by (simp add:sub_path_def)
+      case base thus ?case by (simp add:sub_path_def)
     next
-      case (2 i) thus ?case
+      case (step i) thus ?case
 	by (simp add:sub_path_def upt_rec[of i k] idemp)
     qed