src/HOL/HOLCF/FOCUS/Fstreams.thy
changeset 41855 c3b6e69da386
parent 41476 0fa9629aa399
child 42151 4da4fc77664b
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Sat Feb 26 20:16:44 2011 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Sat Feb 26 20:40:45 2011 +0100
@@ -83,11 +83,11 @@
 lemma jth_n[simp]: "Fin n = #s ==> jth n (s ooo <a>) = a"
 apply (simp add: jth_def, auto)
 apply (simp add: i_th_def rt_sconc1)
-by (simp add: inat_defs split: inat_splits)
+by (simp add: inat_defs split: inat.splits)
 
 lemma last_sconc[simp]: "Fin n = #s ==> last (s ooo <a>) = a"
 apply (simp add: last_def)
-apply (simp add: inat_defs split:inat_splits)
+apply (simp add: inat_defs split:inat.splits)
 by (drule sym, auto)
 
 lemma last_fsingleton[simp]: "last (<a>) = a"
@@ -103,7 +103,7 @@
 by (simp add: last_def)
 
 lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"
-by (simp add: jth_def inat_defs split:inat_splits, auto)
+by (simp add: jth_def inat_defs split:inat.splits, auto)
 
 lemma jth_UU[simp]:"jth n UU = undefined" 
 by (simp add: jth_def)