# HG changeset patch
# User haftmann
# Date 1620675951 0
# Node ID fecfb96474ca014a6b83b94c289523b9aaf09fcf
# Parent  8b3e672df28c9c42851c508de73bc31376086f78
guide is out of focus

diff -r 8b3e672df28c -r fecfb96474ca src/HOL/Combinatorics/Guide.thy
--- a/src/HOL/Combinatorics/Guide.thy	Mon May 10 22:32:02 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-
-section \<open>Basic combinatorics in Isabelle/HOL (and the Archive of Formal Proofs)\<close>
-
-theory Guide
-imports Combinatorics
-begin
-
-end
diff -r 8b3e672df28c -r fecfb96474ca src/HOL/ROOT
--- a/src/HOL/ROOT	Mon May 10 22:32:02 2021 +0200
+++ b/src/HOL/ROOT	Mon May 10 19:45:51 2021 +0000
@@ -131,7 +131,6 @@
     "HOL-Library"
   theories
     Combinatorics
-    Guide
   document_files
     "root.tex"