# HG changeset patch
# User nipkow
# Date 1587676109 -7200
# Node ID 641f4c8ffec8be0d347099b55aa9c870bfdbcc41
# Parent  8ad9b2d3dd81fad3f0166e961c5d7cdb102aa221
tuned document

diff -r 8ad9b2d3dd81 -r 641f4c8ffec8 src/HOL/Data_Structures/Tree2.thy
--- a/src/HOL/Data_Structures/Tree2.thy	Thu Apr 23 22:54:23 2020 +0200
+++ b/src/HOL/Data_Structures/Tree2.thy	Thu Apr 23 23:08:29 2020 +0200
@@ -1,3 +1,5 @@
+section \<open>Augmented Tree (Tree2)\<close>
+
 theory Tree2
 imports "HOL-Library.Tree"
 begin