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/Library/Sublist.thy
changeset 82691 b69e4da2604b
parent 82310 41f5266e5595 
--- a/src/HOL/Library/Sublist.thy	Fri Jun 06 18:36:29 2025 +0100
+++ b/src/HOL/Library/Sublist.thy	Mon Jun 09 22:14:38 2025 +0200
@@ -1462,7 +1462,7 @@
   case (1 P xs ys)
   show ?case
     by (induction ys arbitrary: xs)
-       (auto simp: list_emb_code List.null_def split: list.splits)
+       (auto simp: list_emb_code split: list.splits)
 qed
 
 lemma prefix_transfer [transfer_rule]:
isabelle