     1.1 --- a/src/ZF/OrderType.thy	Tue Jun 01 18:52:38 2004 +0200
     1.2 +++ b/src/ZF/OrderType.thy	Wed Jun 02 17:35:08 2004 +0200
     1.3 @@ -812,10 +812,11 @@
     1.4   prefer 2
     1.5   apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2)
     1.6  apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2)
     1.7 -apply (rule bexI)
     1.8 -prefer 2 apply (blast elim!: ltE)
     1.9 +apply (rule bexI [of _ i']) 
    1.10 +apply (rule bexI [of _ j']) 
    1.11  apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric])
    1.12  apply (simp add: lt_Ord lt_Ord2 raw_oadd_eq_oadd)
    1.13 +apply (simp_all add: lt_def) 
    1.14  done
    1.15  
    1.16  lemma omult_unfold:
changeset 14864	419b45cdb400
parent 14052	e9c9f69e4f63
child 16417	9bc16273c2d4