src/ZF/Constructible/Rec_Separation.thy
changeset 29223 e09c53289830
parent 21404 eb85850d3eb7
child 30729 461ee3e49ad3
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Dec 10 17:19:25 2008 +0100
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Dec 11 18:30:26 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      ZF/Constructible/Rec_Separation.thy
     1.5 -    ID:   $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7  *)
     1.8  
     1.9 @@ -186,7 +185,7 @@
    1.10  theorem M_trancl_L: "PROP M_trancl(L)"
    1.11  by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
    1.12  
    1.13 -interpretation M_trancl [L] by (rule M_trancl_L)
    1.14 +interpretation L: M_trancl L by (rule M_trancl_L)
    1.15  
    1.16  
    1.17  subsection{*@{term L} is Closed Under the Operator @{term list}*}
    1.18 @@ -373,7 +372,7 @@
    1.19    apply (rule M_datatypes_axioms_L) 
    1.20    done
    1.21  
    1.22 -interpretation M_datatypes [L] by (rule M_datatypes_L)
    1.23 +interpretation L: M_datatypes L by (rule M_datatypes_L)
    1.24  
    1.25  
    1.26  subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
    1.27 @@ -436,7 +435,7 @@
    1.28    apply (rule M_eclose_axioms_L)
    1.29    done
    1.30  
    1.31 -interpretation M_eclose [L] by (rule M_eclose_L)
    1.32 +interpretation L: M_eclose L by (rule M_eclose_L)
    1.33  
    1.34  
    1.35  end