src/ZF/Constructible/Datatype_absolute.thy
changeset 13615 449a70d88b38
parent 13564 1500a2e48d44
child 13634 99a593b49b04
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Oct 01 11:17:25 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Oct 01 13:26:10 2002 +0200
     1.3 @@ -683,10 +683,8 @@
     1.4       Ord(i);  M(i);  M(z);
     1.5       \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
     1.6     ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)" 
     1.7 -apply (rotate_tac 2) 
     1.8 -apply (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
     1.9 +by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
    1.10         transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
    1.11 -done
    1.12  
    1.13  
    1.14  theorem (in M_eclose) transrec_closed:
    1.15 @@ -694,10 +692,9 @@
    1.16  	Ord(i);  M(i);  
    1.17  	\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
    1.18        ==> M(transrec(i,H))"
    1.19 -apply (rotate_tac 2) 
    1.20 -apply (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
    1.21 -       transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
    1.22 -done
    1.23 +by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
    1.24 +        transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
    1.25 +
    1.26  
    1.27  text{*Helps to prove instances of @{term transrec_replacement}*}
    1.28  lemma (in M_eclose) transrec_replacementI: