Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hilbert_Choice.thy
changeset 16796 140f1e0ea846
parent 16563 a92f96951355
child 17420 bdcffa8d8665 
--- a/src/HOL/Hilbert_Choice.thy	Wed Jul 13 15:06:04 2005 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Wed Jul 13 15:06:20 2005 +0200
@@ -336,7 +336,7 @@
     "P k ==> \<exists>x. P x & (\<forall>y. P y --> m x <= (m y::nat))"
   apply (simp only: pred_nat_trancl_eq_le [symmetric])
   apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
-   apply (simp add: less_eq not_le_iff_less pred_nat_trancl_eq_le, assumption)
+   apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le, assumption)
   done
 
 lemma LeastM_nat_lemma:
isabelle