src/HOL/ROOT
changeset 48738 f8c1a5b9488f
parent 48721 866f6d5baf4c
child 48765 fb1ed5230abc
--- a/src/HOL/ROOT	Wed Aug 08 15:58:40 2012 +0200
+++ b/src/HOL/ROOT	Wed Aug 08 17:49:56 2012 +0200
@@ -1,30 +1,30 @@
-session HOL! (main) in "." = Pure +
+session HOL (main) = Pure +
   description {* Classical Higher-order Logic *}
   options [document_graph]
   theories Complex_Main
   files "document/root.bib" "document/root.tex"
 
-session "HOL-Base"! in "." = Pure +
+session "HOL-Base" = Pure +
   description {* Raw HOL base, with minimal tools *}
   options [document = false]
   theories HOL
 
-session "HOL-Plain"! in "." = Pure +
+session "HOL-Plain" = Pure +
   description {* HOL side-entry after bootstrap of many tools and packages *}
   options [document = false]
   theories Plain
 
-session "HOL-Main"! in "." = Pure +
+session "HOL-Main" = Pure +
   description {* HOL side-entry for Main only, without Complex_Main *}
   options [document = false]
   theories Main
 
-session "HOL-Proofs"! in "." = Pure +
+session "HOL-Proofs" = Pure +
   description {* HOL-Main with explicit proof terms *}
   options [document = false, proofs = 2, parallel_proofs = 0]
   theories Main
 
-session Library = HOL +
+session "HOL-Library" in Library = HOL +
   description {* Classical Higher-order Logic -- batteries included *}
   theories
     Library
@@ -41,7 +41,7 @@
     Target_Numeral
   files "document/root.bib" "document/root.tex"
 
-session Hahn_Banach = HOL +
+session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
   description {*
     Author:     Gertrud Bauer, TU Munich
 
@@ -51,7 +51,7 @@
   theories Hahn_Banach
   files "document/root.bib" "document/root.tex"
 
-session Induct = HOL +
+session "HOL-Induct" in Induct = HOL +
   theories [quick_and_dirty]
     Common_Patterns
   theories
@@ -68,7 +68,7 @@
     Com
   files "document/root.tex"
 
-session IMP = HOL +
+session "HOL-IMP" in IMP = HOL +
   options [document_graph]
   theories [document = false]
     "~~/src/HOL/ex/Interpretation_with_Defs"
@@ -109,7 +109,7 @@
     Fold
   files "document/root.bib" "document/root.tex"
 
-session IMPP = HOL +
+session "HOL-IMPP" in IMPP = HOL +
   description {*
     Author:     David von Oheimb
     Copyright   1999 TUM
@@ -117,16 +117,16 @@
   options [document = false]
   theories EvenOdd
 
-session Import = HOL +
+session "HOL-Import" in Import = HOL +
   options [document_graph]
   theories HOL_Light_Maps
   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
 
-session Number_Theory = HOL +
+session "HOL-Number_Theory" in Number_Theory = HOL +
   options [document = false]
   theories Number_Theory
 
-session Old_Number_Theory = HOL +
+session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
   options [document_graph]
   theories [document = false]
     "~~/src/HOL/Library/Infinite_Set"
@@ -142,20 +142,20 @@
     Pocklington
   files "document/root.tex"
 
-session Hoare = HOL +
+session "HOL-Hoare" in Hoare = HOL +
   theories Hoare
   files "document/root.bib" "document/root.tex"
 
-session Hoare_Parallel = HOL +
+session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +
   options [document_graph]
   theories Hoare_Parallel
   files "document/root.bib" "document/root.tex"
 
-session Codegenerator_Test = "HOL-Library" +
+session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   options [document = false, document_graph = false, browser_info = false]
   theories Generate Generate_Pretty RBT_Set_Test
 
-session Metis_Examples = HOL +
+session "HOL-Metis_Examples" in Metis_Examples = HOL +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
@@ -174,7 +174,7 @@
     Trans_Closure
     Sets
 
-session Nitpick_Examples = HOL +
+session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
   description {*
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2009
@@ -182,7 +182,7 @@
   options [document = false]
   theories [quick_and_dirty] Nitpick_Examples
 
-session Algebra = HOL +
+session "HOL-Algebra" in Algebra = HOL +
   description {*
     Author: Clemens Ballarin, started 24 September 1999
 
@@ -212,7 +212,7 @@
     "poly/Polynomial"    (*The full theory*)
   files "document/root.bib" "document/root.tex"
 
-session Auth = HOL +
+session "HOL-Auth" in Auth = HOL +
   options [document_graph]
   theories
     Auth_Shared
@@ -222,7 +222,7 @@
     "Guard/Auth_Guard_Public"
   files "document/root.tex"
 
-session UNITY = HOL +
+session "HOL-UNITY" in UNITY = HOL +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
@@ -268,17 +268,17 @@
     "ELT"
   files "document/root.tex"
 
-session Unix = HOL +
+session "HOL-Unix" in Unix = HOL +
   options [print_mode = "no_brackets,no_type_brackets"]
   theories Unix
   files "document/root.bib" "document/root.tex"
 
-session ZF = HOL +
+session "HOL-ZF" in ZF = HOL +
   description {* *}
   theories MainZF Games
   files "document/root.tex"
 
-session Imperative_HOL = HOL +
+session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
   description {* *}
   options [document_graph, print_mode = "iff,no_brackets"]
   theories [document = false]
@@ -289,15 +289,15 @@
   theories Imperative_HOL_ex
   files "document/root.bib" "document/root.tex"
 
-session Decision_Procs = HOL +
+session "HOL-Decision_Procs" in Decision_Procs = HOL +
   options [condition = ISABELLE_POLYML, document = false]
   theories Decision_Procs
 
-session ex in "Proofs/ex" = "HOL-Proofs" +
+session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   options [document = false, proofs = 2, parallel_proofs = 0]
   theories Hilbert_Classical
 
-session Extraction in "Proofs/Extraction" = "HOL-Proofs" +
+session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
   description {* Examples for program extraction in Higher-Order Logic *}
   options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
   theories [document = false]
@@ -314,7 +314,7 @@
     Euclid
   files "document/root.bib" "document/root.tex"
 
-session Lambda in "Proofs/Lambda" = "HOL-Proofs" +
+session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
   options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0]
   theories [document = false]
     "~~/src/HOL/Library/Code_Integer"
@@ -325,14 +325,14 @@
     WeakNorm
   files "document/root.bib" "document/root.tex"
 
-session Prolog = HOL +
+session "HOL-Prolog" in Prolog = HOL +
   description {*
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   *}
   options [document = false]
   theories Test Type
 
-session MicroJava = HOL +
+session "HOL-MicroJava" in MicroJava = HOL +
   options [document_graph]
   theories [document = false] "~~/src/HOL/Library/While_Combinator"
   theories MicroJava
@@ -341,16 +341,16 @@
     "document/root.bib"
     "document/root.tex"
 
-session "MicroJava-skip_proofs" in MicroJava = HOL +
+session "HOL-MicroJava-skip_proofs" in MicroJava = HOL +
   options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs, quick_and_dirty]
   theories MicroJava
 
-session NanoJava = HOL +
+session "HOL-NanoJava" in NanoJava = HOL +
   options [document_graph]
   theories Example
   files "document/root.bib" "document/root.tex"
 
-session Bali = HOL +
+session "HOL-Bali" in Bali = HOL +
   options [document_graph]
   theories
     AxExample
@@ -359,7 +359,7 @@
     Trans
   files "document/root.tex"
 
-session IOA = HOL +
+session "HOL-IOA" in IOA = HOL +
   description {*
     Author:     Tobias Nipkow & Konrad Slind
     Copyright   1994  TU Muenchen
@@ -388,7 +388,7 @@
   options [document = false]
   theories Solve
 
-session Lattice = HOL +
+session "HOL-Lattice" in Lattice = HOL +
   description {*
     Author:     Markus Wenzel, TU Muenchen
 
@@ -397,7 +397,7 @@
   theories CompleteLattice
   files "document/root.tex"
 
-session ex = HOL +
+session "HOL-ex" in ex = HOL +
   description {* Miscellaneous examples for Higher-Order Logic. *}
   options [timeout = 3600, condition = ISABELLE_POLYML]
   theories [document = false]
@@ -483,7 +483,7 @@
 *)
   files "document/root.bib" "document/root.tex"
 
-session Isar_Examples = HOL +
+session "HOL-Isar_Examples" in Isar_Examples = HOL +
   description {* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *}
   theories [document = false]
     "~~/src/HOL/Library/Lattice_Syntax"
@@ -509,35 +509,35 @@
     "document/root.tex"
     "document/style.tex"
 
-session SET_Protocol = HOL +
+session "HOL-SET_Protocol" in SET_Protocol = HOL +
   options [document_graph]
   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   theories SET_Protocol
   files "document/root.tex"
 
-session Matrix_LP = HOL +
+session "HOL-Matrix_LP" in Matrix_LP = HOL +
   options [document_graph]
   theories Cplex
   files "document/root.tex"
 
-session TLA = HOL +
+session "HOL-TLA" in TLA = HOL +
   description {* The Temporal Logic of Actions *}
   options [document = false]
   theories TLA
 
-session Inc in "TLA/Inc" = "HOL-TLA" +
+session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   options [document = false]
   theories Inc
 
-session Buffer in "TLA/Buffer" = "HOL-TLA" +
+session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   options [document = false]
   theories DBuffer
 
-session Memory in "TLA/Memory" = "HOL-TLA" +
+session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   options [document = false]
   theories MemoryImplementation
 
-session TPTP = HOL +
+session "HOL-TPTP" in TPTP = HOL +
   description {*
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Nik Sultana, University of Cambridge
@@ -555,7 +555,7 @@
   theories [proofs = 0]  (* FIXME !? *)
     ATP_Problem_Import
 
-session Multivariate_Analysis = HOL +
+session "HOL-Multivariate_Analysis" in Multivariate_Analysis = HOL +
   options [document_graph]
   theories
     Multivariate_Analysis
@@ -564,7 +564,7 @@
     "Integration.certs"
     "document/root.tex"
 
-session "HOL-Probability"! in "Probability" = "HOL-Multivariate_Analysis" +
+session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   options [document_graph]
   theories [document = false]
     "~~/src/HOL/Library/Countable"
@@ -576,45 +576,45 @@
     "ex/Koepf_Duermuth_Countermeasure"
   files "document/root.tex"
 
-session Nominal (main) = HOL +
+session "HOL-Nominal" (main) in Nominal = HOL +
   options [document = false]
   theories Nominal
 
-session Examples in "Nominal/Examples" = "HOL-Nominal" +
+session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
   theories Nominal_Examples
   theories [quick_and_dirty] VC_Condition
 
-session Word = HOL +
+session "HOL-Word" in Word = HOL +
   options [document_graph]
   theories Word
   files "document/root.bib" "document/root.tex"
 
-session Examples in "Word/Examples" = "HOL-Word" +
+session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   options [document = false]
   theories WordExamples
 
-session Statespace = HOL +
+session "HOL-Statespace" in Statespace = HOL +
   theories StateSpaceEx
   files "document/root.tex"
 
-session NSA = HOL +
+session "HOL-NSA" in NSA = HOL +
   options [document_graph]
   theories Hypercomplex
   files "document/root.tex"
 
-session Examples in "NSA/Examples" = "HOL-NSA" +
+session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   options [document = false]
   theories NSPrimes
 
-session Mirabelle = HOL +
+session "HOL-Mirabelle" in Mirabelle = HOL +
   options [document = false]
   theories Mirabelle_Test
 
-session ex in "Mirabelle/ex" = "HOL-Mirabelle" +
+session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   theories Ex
 
-session SMT_Examples = "HOL-Word" +
+session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   options [document = false, quick_and_dirty]
   theories
     SMT_Tests
@@ -624,11 +624,11 @@
     "SMT_Examples.certs"
     "SMT_Tests.certs"
 
-session "HOL-Boogie"! in "Boogie" = "HOL-Word" +
+session "HOL-Boogie" in "Boogie" = "HOL-Word" +
   options [document = false]
   theories Boogie
 
-session Examples in "Boogie/Examples" = "HOL-Boogie" +
+session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" +
   options [document = false]
   theories
     Boogie_Max_Stepwise
@@ -643,11 +643,11 @@
     "VCC_Max.b2i"
     "VCC_Max.certs"
 
-session "HOL-SPARK"! in "SPARK" = "HOL-Word" +
+session "HOL-SPARK" in "SPARK" = "HOL-Word" +
   options [document = false]
   theories SPARK
 
-session Examples in "SPARK/Examples" = "HOL-SPARK" +
+session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   options [document = false]
   theories
     "Gcd/Greatest_Common_Divisor"
@@ -700,7 +700,7 @@
     "RIPEMD-160/rmd/s_r.rls"
     "RIPEMD-160/rmd/s_r.siv"
 
-session Manual in "SPARK/Manual" = "HOL-SPARK" +
+session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   options [show_question_marks = false]
   theories
     Example_Verification
@@ -733,11 +733,11 @@
     "simple_greatest_common_divisor/g_c_d.rls"
     "simple_greatest_common_divisor/g_c_d.siv"
 
-session Mutabelle = HOL +
+session "HOL-Mutabelle" in Mutabelle = HOL +
   options [document = false]
   theories MutabelleExtra
 
-session Quickcheck_Examples = HOL +
+session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   options [timeout = 3600, document = false]
   theories
     Quickcheck_Examples
@@ -749,14 +749,14 @@
   theories [condition = ISABELLE_GHC]
     Quickcheck_Narrowing_Examples
 
-session Quickcheck_Benchmark = HOL +
+session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
     Find_Unused_Assms_Examples
     Needham_Schroeder_No_Attacker_Example
     Needham_Schroeder_Guided_Attacker_Example
     Needham_Schroeder_Unguided_Attacker_Example
 
-session Quotient_Examples = HOL +
+session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   description {*
     Author:     Cezary Kaliszyk and Christian Urban
   *}
@@ -772,7 +772,7 @@
     Quotient_Rat
     Lift_DList
 
-session Predicate_Compile_Examples = HOL +
+session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   options [document = false]
   theories
     Examples
@@ -795,7 +795,7 @@
   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
     Reg_Exp_Example
 
-session HOLCF! (main) = HOL +
+session HOLCF (main) in HOLCF = HOL +
   description {*
     Author:     Franz Regensburger
     Author:     Brian Huffman
@@ -812,23 +812,23 @@
     HOLCF
   files "document/root.tex"
 
-session Tutorial in "HOLCF/Tutorial" = HOLCF +
+session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   theories
     Domain_ex
     Fixrec_ex
     New_Domain
   files "document/root.tex"
 
-session Library in "HOLCF/Library" = HOLCF +
+session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   options [document = false]
   theories HOLCF_Library
 
-session IMP in "HOLCF/IMP" = HOLCF +
+session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   options [document = false]
   theories HoareEx
   files "document/root.tex"
 
-session ex in "HOLCF/ex" = HOLCF +
+session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   description {* Misc HOLCF examples *}
   options [document = false]
   theories
@@ -844,14 +844,14 @@
     Letrec
     Pattern_Match
 
-session FOCUS in "HOLCF/FOCUS" = HOLCF +
+session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
   options [document = false]
   theories
     Fstreams
     FOCUS
     Buffer_adm
 
-session IOA! in "HOLCF/IOA" = HOLCF +
+session IOA in "HOLCF/IOA" = HOLCF +
   description {*
     Author:     Olaf Mueller
 
@@ -860,7 +860,7 @@
   options [document = false]
   theories "meta_theory/Abstraction"
 
-session ABP in "HOLCF/IOA/ABP" = IOA +
+session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   description {*
     Author:     Olaf Mueller
 
@@ -869,7 +869,7 @@
   options [document = false]
   theories Correctness
 
-session NTP in "HOLCF/IOA/NTP" = IOA +
+session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
   description {*
     Author:     Tobias Nipkow & Konrad Slind
 
@@ -879,7 +879,7 @@
   options [document = false]
   theories Correctness
 
-session Storage in "HOLCF/IOA/Storage" = IOA +
+session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
   description {*
     Author:     Olaf Mueller
 
@@ -888,7 +888,7 @@
   options [document = false]
   theories Correctness
 
-session ex in "HOLCF/IOA/ex" = IOA +
+session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
   description {*
     Author:     Olaf Mueller
   *}
@@ -897,7 +897,7 @@
     TrivEx
     TrivEx2
 
-session Datatype_Benchmark = HOL +
+session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
   description {* Some rather large datatype examples (from John Harrison). *}
   options [document = false]
   theories [condition = ISABELLE_FULL_TEST, timing]
@@ -906,7 +906,7 @@
     SML
     Verilog
 
-session Record_Benchmark = HOL +
+session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
   description {* Some benchmark on large record. *}
   options [document = false]
   theories [condition = ISABELLE_FULL_TEST, timing]