src/HOL/ROOT
changeset 72515 c7038c397ae3
parent 72486 e4d707eb7d1b
child 72536 589645894305
equal deleted inserted replaced
72514:d8661799afb2 72515:c7038c397ae3
   322 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   322 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   323   sessions
   323   sessions
   324     "HOL-Number_Theory"
   324     "HOL-Number_Theory"
   325     "HOL-Data_Structures"
   325     "HOL-Data_Structures"
   326     "HOL-Examples"
   326     "HOL-Examples"
   327     "HOL-Word"
       
   328   theories
   327   theories
   329     Generate
   328     Generate
   330     Generate_Binary_Nat
   329     Generate_Binary_Nat
   331     Generate_Target_Nat
   330     Generate_Target_Nat
   332     Generate_Efficient_Datastructures
   331     Generate_Efficient_Datastructures
   613 
   612 
   614 session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
   613 session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
   615   description "
   614   description "
   616     Miscellaneous examples for Higher-Order Logic.
   615     Miscellaneous examples for Higher-Order Logic.
   617   "
   616   "
   618   sessions
       
   619     "HOL-Word"
       
   620   theories
   617   theories
   621     Antiquote
   618     Antiquote
   622     Argo_Examples
   619     Argo_Examples
   623     Arith_Examples
   620     Arith_Examples
   624     Ballot
   621     Ballot
   890     "Tests/Small_Concrete"
   887     "Tests/Small_Concrete"
   891     "Tests/Stream_Friends"
   888     "Tests/Stream_Friends"
   892     "Tests/TLList_Friends"
   889     "Tests/TLList_Friends"
   893     "Tests/Type_Class"
   890     "Tests/Type_Class"
   894 
   891 
   895 session "HOL-Word" (main timing) in Word = HOL +
       
   896   sessions
       
   897     "HOL-Library"
       
   898   theories
       
   899     Word
       
   900     More_Word
       
   901     Word_Examples
       
   902   document_files "root.bib" "root.tex"
       
   903 
       
   904 session "HOL-Statespace" in Statespace = HOL +
   892 session "HOL-Statespace" in Statespace = HOL +
   905   theories [skip_proofs = false]
   893   theories [skip_proofs = false]
   906     StateSpaceEx
   894     StateSpaceEx
   907   document_files "root.tex"
   895   document_files "root.tex"
   908 
   896 
   923 
   911 
   924 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   912 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   925   options [timeout = 60]
   913   options [timeout = 60]
   926   theories Ex
   914   theories Ex
   927 
   915 
   928 session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" +
   916 session "HOL-SMT_Examples" (timing) in SMT_Examples = HOL +
   929   options [quick_and_dirty]
   917   options [quick_and_dirty]
       
   918   sessions
       
   919     "HOL-Library"
   930   theories
   920   theories
   931     Boogie
   921     Boogie
   932     SMT_Examples
   922     SMT_Examples
   933     SMT_Word_Examples
   923     SMT_Word_Examples
   934     SMT_Tests
   924     SMT_Tests
   935     SMT_Tests_Verit
   925     SMT_Tests_Verit
   936     SMT_Examples_Verit
   926     SMT_Examples_Verit
   937 
   927 
   938 session "HOL-SPARK" in "SPARK" = "HOL-Word" +
   928 session "HOL-SPARK" in "SPARK" = HOL +
       
   929   sessions
       
   930     "HOL-Library"
   939   theories
   931   theories
   940     SPARK
   932     SPARK
   941 
   933 
   942 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   934 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   943   directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt"
   935   directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt"
   957   export_files (in ".") "*:**.prv"
   949   export_files (in ".") "*:**.prv"
   958 
   950 
   959 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   951 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   960   options [show_question_marks = false]
   952   options [show_question_marks = false]
   961   sessions
   953   sessions
       
   954     "HOL-Library"
   962     "HOL-SPARK-Examples"
   955     "HOL-SPARK-Examples"
   963   theories
   956   theories
   964     Example_Verification
   957     Example_Verification
   965     VC_Principles
   958     VC_Principles
   966     Reference
   959     Reference