src/HOL/Hilbert_Choice.thy
changeset 16796 140f1e0ea846
parent 16563 a92f96951355
child 17420 bdcffa8d8665
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Jul 13 15:06:04 2005 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Jul 13 15:06:20 2005 +0200
     1.3 @@ -336,7 +336,7 @@
     1.4      "P k ==> \<exists>x. P x & (\<forall>y. P y --> m x <= (m y::nat))"
     1.5    apply (simp only: pred_nat_trancl_eq_le [symmetric])
     1.6    apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
     1.7 -   apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le, assumption)
     1.8 +   apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le, assumption)
     1.9    done
    1.10  
    1.11  lemma LeastM_nat_lemma: