# HG changeset patch
# User wenzelm
# Date 1596793574 -7200
# Node ID 16fab31feadc8c06e69a99077e960773810f6527
# Parent  ae683a461c4006f4472b417e0f676494263de1c3
avoid failure of "isabelle build -o skip_proofs";

diff -r ae683a461c40 -r 16fab31feadc src/HOL/Data_Structures/AVL_Set.thy
--- 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"