src/HOLCF/IOA/meta_theory/Sequence.thy
changeset 30607 c3d1590debd8
parent 27239 f2f42f9fa09d
child 30807 a167ed35ec0d
     1.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Olaf Müller
     1.7  
     1.8  Sequences over flat domains with lifted elements.
     1.9 @@ -340,7 +339,7 @@
    1.10  lemma Seq_induct:
    1.11  "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x"
    1.12  apply (erule (2) seq.ind)
    1.13 -apply (tactic {* def_tac 1 *})
    1.14 +apply defined
    1.15  apply (simp add: Consq_def)
    1.16  done
    1.17  
    1.18 @@ -348,14 +347,14 @@
    1.19  "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]
    1.20                  ==> seq_finite x --> P x"
    1.21  apply (erule (1) seq_finite_ind)
    1.22 -apply (tactic {* def_tac 1 *})
    1.23 +apply defined
    1.24  apply (simp add: Consq_def)
    1.25  done
    1.26  
    1.27  lemma Seq_Finite_ind:
    1.28  "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x"
    1.29  apply (erule (1) Finite.induct)
    1.30 -apply (tactic {* def_tac 1 *})
    1.31 +apply defined
    1.32  apply (simp add: Consq_def)
    1.33  done
    1.34