src/ZF/Constructible/L_axioms.thy

   apply (rule M_trivial_axioms.intro)
       apply (rule upair_ax)
    apply (rule Union_ax)
   done
 
-interpretation L?: M_trivial L by (rule M_trivial_L)
+interpretation L: M_trivial L by (rule M_trivial_L)
 
 (* Replaces the following declarations...
 lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]
   and rex_abs = M_trivial.rex_abs [OF M_trivial_L]
 ...