# HG changeset patch
# User huffman
# Date 1267590967 28800
# Node ID 60647586b1732f09bfb1d7240c71ec4e545fdc05
# Parent  4b7d5b88a96591e7735d54131efc058cfcb240cc
adapt to changed variable name in casedist theorem

diff -r 4b7d5b88a965 -r 60647586b173 src/HOLCF/FOCUS/Fstream.thy
--- a/src/HOLCF/FOCUS/Fstream.thy	Tue Mar 02 20:19:04 2010 -0800
+++ b/src/HOLCF/FOCUS/Fstream.thy	Tue Mar 02 20:36:07 2010 -0800
@@ -83,7 +83,7 @@
 by (simp add: fscons_def2)
 
 lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt &  s << tt"
-apply (rule_tac x="t" in stream.casedist)
+apply (cases t)
 apply (cut_tac fscons_not_empty)
 apply (fast dest: eq_UU_iff [THEN iffD2])
 apply (simp add: fscons_def2)
diff -r 4b7d5b88a965 -r 60647586b173 src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Mar 02 20:19:04 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Mar 02 20:36:07 2010 -0800
@@ -191,7 +191,7 @@
 by simp
 
 lemma nil_less_is_nil: "nil<<x ==> nil=x"
-apply (rule_tac x="x" in seq.casedist)
+apply (cases x)
 apply simp
 apply simp
 apply simp
@@ -286,8 +286,8 @@
 
 lemma Finite_upward: "\<lbrakk>Finite x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> Finite y"
 apply (induct arbitrary: y set: Finite)
-apply (rule_tac x=y in seq.casedist, simp, simp, simp)
-apply (rule_tac x=y in seq.casedist, simp, simp)
+apply (case_tac y, simp, simp, simp)
+apply (case_tac y, simp, simp)
 apply simp
 done
 
diff -r 4b7d5b88a965 -r 60647586b173 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Tue Mar 02 20:19:04 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Tue Mar 02 20:36:07 2010 -0800
@@ -163,8 +163,7 @@
 
 lemma Last_cons: "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"
 apply (simp add: Last_def Consq_def)
-apply (rule_tac x="xs" in seq.casedist)
-apply simp
+apply (cases xs)
 apply simp_all
 done
 
@@ -208,7 +207,7 @@
 lemma Zip_UU2: "x~=nil ==> Zip$x$UU =UU"
 apply (subst Zip_unfold)
 apply simp
-apply (rule_tac x="x" in seq.casedist)
+apply (cases x)
 apply simp_all
 done
 
diff -r 4b7d5b88a965 -r 60647586b173 src/HOLCF/ex/Dnat.thy
--- a/src/HOLCF/ex/Dnat.thy	Tue Mar 02 20:19:04 2010 -0800
+++ b/src/HOLCF/ex/Dnat.thy	Tue Mar 02 20:36:07 2010 -0800
@@ -55,12 +55,12 @@
   apply (induct_tac x rule: dnat.ind)
     apply fast
    apply (rule allI)
-   apply (rule_tac x = y in dnat.casedist)
+   apply (case_tac y)
      apply simp
     apply simp
    apply simp
   apply (rule allI)
-  apply (rule_tac x = y in dnat.casedist)
+  apply (case_tac y)
     apply (fast intro!: UU_I)
    apply (thin_tac "ALL y. dnat << y --> dnat = UU | dnat = y")
    apply simp