src/ZF/Constructible/Rank_Separation.thy

        apply (assumption | rule well_ord_iso_separation
          obase_separation obase_equals_separation
          omap_replacement)+
   done
 
-theorem M_ordertype_L: "PROP M_ordertype(L)"
+theorem M_ordertype_L: "M_ordertype(L)"
   apply (rule M_ordertype.intro)
    apply (rule M_basic_L)
   apply (rule M_ordertype_axioms_L) 
   done
 

   apply (rule M_wfrank_axioms.intro)
    apply (assumption | rule
      wfrank_separation wfrank_strong_replacement Ord_wfrank_separation)+
   done
 
-theorem M_wfrank_L: "PROP M_wfrank(L)"
+theorem M_wfrank_L: "M_wfrank(L)"
   apply (rule M_wfrank.intro)
    apply (rule M_trancl_L)
   apply (rule M_wfrank_axioms_L) 
   done