clarified session: avoid merge of different syntax from different Hoare logics;

--- a/src/HOL/Hoare/Hoare.thy	Wed Dec 23 17:16:05 2020 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(*  Author:     Tobias Nipkow
-    Copyright   1998-2003 TUM
-*)
-
-theory Hoare
-imports Examples ExamplesAbort ExamplesTC Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation
-begin
-
-end

--- a/src/HOL/ROOT	Wed Dec 23 17:16:05 2020 +0100
+++ b/src/HOL/ROOT	Wed Dec 23 20:49:05 2020 +0100
@@ -311,7 +311,15 @@
     Verification of imperative programs (verification conditions are generated
     automatically from pre/post conditions and loop invariants).
   "
-  theories Hoare
+  theories
+    Examples
+    ExamplesAbort
+    ExamplesTC
+    Pointers0
+    Pointer_Examples
+    Pointer_ExamplesAbort
+    SchorrWaite
+    Separation
   document_files "root.bib" "root.tex"
 
 session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL +