src/HOLCF/IOA/meta_theory/Sequence.thy

 apply (simp add: Consq_def)
 done
 
 lemma Seq_exhaust: "x = UU | x = nil | (? a s. x = a >> s)"
 apply (simp add: Consq_def2)
-apply (cut_tac seq.exhaust)
+apply (cut_tac seq.nchotomy)
 apply (fast dest: not_Undef_is_Def [THEN iffD1])
 done
 
 
 lemma Seq_cases:

 
 subsection "induction"
 
 lemma Seq_induct:
 "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x"
-apply (erule (2) seq.ind)
+apply (erule (2) seq.induct)
 apply defined
 apply (simp add: Consq_def)
 done
 
 lemma Seq_FinitePartial_ind:

 lemma Conc_assoc: "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z"
 apply (rule_tac x="x" in Seq_induct, simp_all)
 done
 
 lemma nilConc [simp]: "s@@ nil = s"
-apply (rule_tac x="s" in seq.ind)
+apply (induct s)
 apply simp
 apply simp
 apply simp
 apply simp
 done