src/ZF/Constructible/Separation.thy
changeset 29223 e09c53289830
parent 19931 fb32b43e7f80
child 30729 461ee3e49ad3
     1.1 --- a/src/ZF/Constructible/Separation.thy	Wed Dec 10 17:19:25 2008 +0100
     1.2 +++ b/src/ZF/Constructible/Separation.thy	Thu Dec 11 18:30:26 2008 +0100
     1.3 @@ -305,7 +305,7 @@
     1.4  theorem M_basic_L: "PROP M_basic(L)"
     1.5  by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
     1.6  
     1.7 -interpretation M_basic [L] by (rule M_basic_L)
     1.8 +interpretation L: M_basic L by (rule M_basic_L)
     1.9  
    1.10  
    1.11  end