guide is out of focus
authorhaftmann
Mon, 10 May 2021 19:45:51 +0000
changeset 73918 fecfb96474ca
parent 73917 8b3e672df28c
child 73919 7734c442802f
guide is out of focus
src/HOL/Combinatorics/Guide.thy
src/HOL/ROOT
--- 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
--- 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"