Mercurial Mercurial > hg > lexing / 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.
thys4/posix/FBound.thy
changeset 601 ce4e5151a836
parent 600 fd068f39ac23
child 618 233cf2b97d1a 
--- a/thys4/posix/FBound.thy	Mon Sep 12 23:32:18 2022 +0200
+++ b/thys4/posix/FBound.thy	Thu Sep 22 00:31:09 2022 +0100
@@ -619,7 +619,8 @@
   by (simp add: scomp_size_reduction)
   
 lemma leq1_eq1_equal:
-  shows "\<lbrakk>r1 \<le>1 r2;
+  shows "\<lbrakk>r1 \<le>1 r2; bsimp r2 = r1 \<rbrakk> \<Longrightarrow> r1 = r2 \<or> s_complexity r1 < s_complexity r2"
+  sorry
lexing