Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added lemma
authornipkow
Mon, 11 Jun 2018 08:15:43 +0200
changeset 68411 d8363de26567
parent 68410 4e27f5c361d2
child 68412 07f8c09e3f79
child 68413 b56ed5010e69
child 68416 33114721ac9a
child 68424 02e5a44ffe7d
added lemma
src/HOL/Data_Structures/Tree2.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Data_Structures/Tree2.thy	Sat Jun 09 21:52:16 2018 +0200
+++ b/src/HOL/Data_Structures/Tree2.thy	Mon Jun 11 08:15:43 2018 +0200
@@ -33,4 +33,7 @@
 lemma size1_ge0[simp]: "0 < size1 t"
 by (simp add: size1_def)
 
+lemma finite_set_tree[simp]: "finite(set_tree t)"
+by(induction t) auto
+
 end
isabelle