--- a/src/CCL/ROOT Sun Sep 08 13:07:03 2019 +0200
+++ b/src/CCL/ROOT Sun Sep 08 16:49:05 2019 +0200
@@ -10,6 +10,7 @@
A computational logic for an untyped functional language with
evaluation to weak head-normal form.
"
+ directories "ex"
sessions
FOL
theories
--- a/src/CTT/ROOT Sun Sep 08 13:07:03 2019 +0200
+++ b/src/CTT/ROOT Sun Sep 08 16:49:05 2019 +0200
@@ -16,6 +16,7 @@
Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
1991)
"
+ directories "ex"
options [thy_output_source]
theories
CTT
--- a/src/Doc/ROOT Sun Sep 08 13:07:03 2019 +0200
+++ b/src/Doc/ROOT Sun Sep 08 16:49:05 2019 +0200
@@ -404,6 +404,8 @@
"root.tex"
session Tutorial (doc) in "Tutorial" = HOL +
+ directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr"
+ "Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
theories [threads = 1]
"ToyList/ToyList_Test"
--- a/src/FOL/ROOT Sun Sep 08 13:07:03 2019 +0200
+++ b/src/FOL/ROOT Sun Sep 08 16:49:05 2019 +0200
@@ -24,6 +24,7 @@
description "
Examples for First-Order Logic.
"
+ directories "Locale_Test"
theories
Natural_Numbers
Intro
@@ -42,4 +43,3 @@
theories [document = false, skip_proofs = false]
"Locale_Test/Locale_Test"
document_files "root.tex"
-
--- a/src/HOL/ROOT Sun Sep 08 13:07:03 2019 +0200
+++ b/src/HOL/ROOT Sun Sep 08 16:49:05 2019 +0200
@@ -4,6 +4,7 @@
description "
Classical Higher-order Logic.
"
+ directories "../Tools"
options [strict_facts]
theories [dump_checkpoint]
Main (global)
@@ -349,6 +350,7 @@
description "
A new approach to verifying authentication protocols.
"
+ directories "Smartcard" "Guard"
theories
Auth_Shared
Auth_Public
@@ -364,6 +366,7 @@
Verifying security protocols using Chandy and Misra's UNITY formalism.
"
+ directories "Simple" "Comp"
theories
(*Basic meta-theory*)
UNITY_Main
@@ -413,6 +416,7 @@
document_files "root.tex"
session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" +
+ directories "ex"
options [print_mode = "iff,no_brackets"]
theories Imperative_HOL_ex
document_files "root.bib" "root.tex"
@@ -421,6 +425,7 @@
description "
Various decision procedures, typically involving reflection.
"
+ directories "ex"
theories
Decision_Procs
@@ -485,6 +490,7 @@
machine and a specification of its bytecode verifier and a lightweight
bytecode verifier, including proofs of type-safety.
"
+ directories "BV" "Comp" "DFA" "J" "JVM"
sessions
"HOL-Eisbach"
theories
@@ -700,6 +706,7 @@
description "
Two-dimensional matrices and linear programming.
"
+ directories "Compute_Oracle"
theories Cplex
document_files "root.tex"
@@ -791,6 +798,7 @@
description "
(Co)datatype Examples.
"
+ directories "Derivation_Trees"
theories
Compat
Lambda_Term
@@ -811,6 +819,7 @@
description "
Corecursion Examples.
"
+ directories "Tests"
theories
LFilter
Paper_Examples
@@ -874,6 +883,7 @@
SPARK
session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
+ directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt"
theories
"Gcd/Greatest_Common_Divisor"
"Liseq/Longest_Increasing_Subsequence"
@@ -968,6 +978,7 @@
description "
Experimental extension of Higher-Order Logic to allow translation of types to sets.
"
+ directories "Examples"
theories
Types_To_Sets
"Examples/Prerequisites"
--- a/src/LCF/ROOT Sun Sep 08 13:07:03 2019 +0200
+++ b/src/LCF/ROOT Sun Sep 08 16:49:05 2019 +0200
@@ -10,6 +10,7 @@
Useful references on LCF: Lawrence C. Paulson,
Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
"
+ directories "ex"
sessions
FOL
theories
--- a/src/Sequents/ROOT Sun Sep 08 13:07:03 2019 +0200
+++ b/src/Sequents/ROOT Sun Sep 08 16:49:05 2019 +0200
@@ -37,6 +37,7 @@
S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
of Cambridge Computer Lab, 1995, ed L. Paulson)
"
+ directories "LK"
theories
LK
ILL