--- a/src/HOL/HOL.thy Sat Oct 12 22:20:39 2019 +0200
+++ b/src/HOL/HOL.thy Sun Oct 13 16:26:31 2019 +0200
@@ -5,7 +5,7 @@
section \<open>The basis of Higher-Order Logic\<close>
theory HOL
-imports Pure "~~/src/Tools/Code_Generator"
+imports Pure Tools.Code_Generator
keywords
"try" "solve_direct" "quickcheck" "print_coercions" "print_claset"
"print_induct_rules" :: diag and
--- a/src/HOL/ROOT Sat Oct 12 22:20:39 2019 +0200
+++ b/src/HOL/ROOT Sun Oct 13 16:26:31 2019 +0200
@@ -5,7 +5,7 @@
Classical Higher-order Logic.
"
options [strict_facts]
- directories "../Tools"
+ sessions Tools
theories
Main (global)
Complex_Main (global)
--- a/src/Tools/ROOT Sat Oct 12 22:20:39 2019 +0200
+++ b/src/Tools/ROOT Sun Oct 13 16:26:31 2019 +0200
@@ -1,5 +1,9 @@
chapter Tools
+session Tools = Pure +
+ theories
+ Code_Generator
+
session Spec_Check in Spec_Check = Pure +
theories
Spec_Check