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