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.
avoid failure of "isabelle build -o skip_proofs";
authorwenzelm
Fri, 07 Aug 2020 11:46:14 +0200
changeset 72110 16fab31feadc
parent 72109 ae683a461c40
child 72111 b9ded33bd58c
avoid failure of "isabelle build -o skip_proofs";
src/HOL/Data_Structures/AVL_Set.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Data_Structures/AVL_Set.thy	Thu Aug 06 23:46:57 2020 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Fri Aug 07 11:46:14 2020 +0200
@@ -299,7 +299,7 @@
   case 2
   then show ?case by (simp add: \<phi>_def real_le_lsqrt)
 next
-  case (3 n) term ?case
+  case (3 n)
   have "\<phi> ^ Suc (Suc n) = \<phi> ^ 2 * \<phi> ^ n"
     by (simp add: field_simps power2_eq_square)
   also have "\<dots> = (\<phi> + 1) * \<phi> ^ n"
isabelle