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/Doc/Codegen/Foundations.thy
changeset 82774 2865a6618cba
parent 76673 059a68d21f0f 
--- a/src/Doc/Codegen/Foundations.thy	Thu Jun 26 17:25:29 2025 +0200
+++ b/src/Doc/Codegen/Foundations.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -273,9 +273,9 @@
     of (Some x, q') \<Rightarrow> (x, q'))"
 
 lemma %quote strict_dequeue_AQueue [code]:
-  "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
   "strict_dequeue (AQueue xs []) =
     (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
+  "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
   by (simp_all add: strict_dequeue_def) (cases xs, simp_all split: list.split)
 
 text \<open>
isabelle