# HG changeset patch
# User wenzelm
# Date 1608752945 -3600
# Node ID d231d71d27b4621e141a39447eb12ae5888b2b54
# Parent  9cc431444435c726d6e9b84d848804c73783c458
clarified session: avoid merge of different syntax from different Hoare logics;

diff -r 9cc431444435 -r d231d71d27b4 src/HOL/Hoare/Hoare.thy
--- 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
diff -r 9cc431444435 -r d231d71d27b4 src/HOL/ROOT
--- 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 +