src/ZF/Constructible/Wellorderings.thy
changeset 13295 ca2e9b273472
parent 13293 09276ee04361
child 13298 b4f370679c65
     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Thu Jul 04 11:13:56 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Thu Jul 04 15:03:03 2002 +0200
     1.3 @@ -295,7 +295,7 @@
     1.4  
     1.5  
     1.6  text{*Surely a shorter proof using lemmas in @{text Order}?
     1.7 -     Like well_ord_iso_preserving?*}
     1.8 +     Like @{text well_ord_iso_preserving}?*}
     1.9  lemma (in M_axioms) ord_iso_pred_imp_lt:
    1.10       "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
    1.11         g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));