src/HOL/ROOT
changeset 70675 efd995488228
parent 70669 abdf3732f6f1
child 70678 36c8c32346cb
equal deleted inserted replaced
70674:29bb1ebb188f 70675:efd995488228
     2 
     2 
     3 session HOL (main) = Pure +
     3 session HOL (main) = Pure +
     4   description "
     4   description "
     5     Classical Higher-order Logic.
     5     Classical Higher-order Logic.
     6   "
     6   "
       
     7   directories "../Tools"
     7   options [strict_facts]
     8   options [strict_facts]
     8   theories [dump_checkpoint]
     9   theories [dump_checkpoint]
     9     Main (global)
    10     Main (global)
    10     Complex_Main (global)
    11     Complex_Main (global)
    11   document_files
    12   document_files
   347 
   348 
   348 session "HOL-Auth" (timing) in Auth = "HOL-Library" +
   349 session "HOL-Auth" (timing) in Auth = "HOL-Library" +
   349   description "
   350   description "
   350     A new approach to verifying authentication protocols.
   351     A new approach to verifying authentication protocols.
   351   "
   352   "
       
   353   directories "Smartcard" "Guard"
   352   theories
   354   theories
   353     Auth_Shared
   355     Auth_Shared
   354     Auth_Public
   356     Auth_Public
   355     "Smartcard/Auth_Smartcard"
   357     "Smartcard/Auth_Smartcard"
   356     "Guard/Auth_Guard_Shared"
   358     "Guard/Auth_Guard_Shared"
   362     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   364     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   363     Copyright   1998  University of Cambridge
   365     Copyright   1998  University of Cambridge
   364 
   366 
   365     Verifying security protocols using Chandy and Misra's UNITY formalism.
   367     Verifying security protocols using Chandy and Misra's UNITY formalism.
   366   "
   368   "
       
   369   directories "Simple" "Comp"
   367   theories
   370   theories
   368     (*Basic meta-theory*)
   371     (*Basic meta-theory*)
   369     UNITY_Main
   372     UNITY_Main
   370 
   373 
   371     (*Simple examples: no composition*)
   374     (*Simple examples: no composition*)
   411     MainZF
   414     MainZF
   412     Games
   415     Games
   413   document_files "root.tex"
   416   document_files "root.tex"
   414 
   417 
   415 session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" +
   418 session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" +
       
   419   directories "ex"
   416   options [print_mode = "iff,no_brackets"]
   420   options [print_mode = "iff,no_brackets"]
   417   theories Imperative_HOL_ex
   421   theories Imperative_HOL_ex
   418   document_files "root.bib" "root.tex"
   422   document_files "root.bib" "root.tex"
   419 
   423 
   420 session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
   424 session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
   421   description "
   425   description "
   422     Various decision procedures, typically involving reflection.
   426     Various decision procedures, typically involving reflection.
   423   "
   427   "
       
   428   directories "ex"
   424   theories
   429   theories
   425     Decision_Procs
   430     Decision_Procs
   426 
   431 
   427 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   432 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   428   sessions
   433   sessions
   483   description "
   488   description "
   484     Formalization of a fragment of Java, together with a corresponding virtual
   489     Formalization of a fragment of Java, together with a corresponding virtual
   485     machine and a specification of its bytecode verifier and a lightweight
   490     machine and a specification of its bytecode verifier and a lightweight
   486     bytecode verifier, including proofs of type-safety.
   491     bytecode verifier, including proofs of type-safety.
   487   "
   492   "
       
   493   directories "BV" "Comp" "DFA" "J" "JVM"
   488   sessions
   494   sessions
   489     "HOL-Eisbach"
   495     "HOL-Eisbach"
   490   theories
   496   theories
   491     MicroJava
   497     MicroJava
   492   document_files
   498   document_files
   698 
   704 
   699 session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
   705 session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" +
   700   description "
   706   description "
   701     Two-dimensional matrices and linear programming.
   707     Two-dimensional matrices and linear programming.
   702   "
   708   "
       
   709   directories "Compute_Oracle"
   703   theories Cplex
   710   theories Cplex
   704   document_files "root.tex"
   711   document_files "root.tex"
   705 
   712 
   706 session "HOL-TLA" in TLA = HOL +
   713 session "HOL-TLA" in TLA = HOL +
   707   description "
   714   description "
   789 
   796 
   790 session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
   797 session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
   791   description "
   798   description "
   792     (Co)datatype Examples.
   799     (Co)datatype Examples.
   793   "
   800   "
       
   801   directories "Derivation_Trees"
   794   theories
   802   theories
   795     Compat
   803     Compat
   796     Lambda_Term
   804     Lambda_Term
   797     Process
   805     Process
   798     TreeFsetI
   806     TreeFsetI
   809 
   817 
   810 session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
   818 session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
   811   description "
   819   description "
   812     Corecursion Examples.
   820     Corecursion Examples.
   813   "
   821   "
       
   822   directories "Tests"
   814   theories
   823   theories
   815     LFilter
   824     LFilter
   816     Paper_Examples
   825     Paper_Examples
   817     Stream_Processor
   826     Stream_Processor
   818     "Tests/Simple_Nesting"
   827     "Tests/Simple_Nesting"
   872 session "HOL-SPARK" in "SPARK" = "HOL-Word" +
   881 session "HOL-SPARK" in "SPARK" = "HOL-Word" +
   873   theories
   882   theories
   874     SPARK
   883     SPARK
   875 
   884 
   876 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   885 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
       
   886   directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt"
   877   theories
   887   theories
   878     "Gcd/Greatest_Common_Divisor"
   888     "Gcd/Greatest_Common_Divisor"
   879     "Liseq/Longest_Increasing_Subsequence"
   889     "Liseq/Longest_Increasing_Subsequence"
   880     "RIPEMD-160/F"
   890     "RIPEMD-160/F"
   881     "RIPEMD-160/Hash"
   891     "RIPEMD-160/Hash"
   966 
   976 
   967 session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
   977 session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
   968   description "
   978   description "
   969     Experimental extension of Higher-Order Logic to allow translation of types to sets.
   979     Experimental extension of Higher-Order Logic to allow translation of types to sets.
   970   "
   980   "
       
   981   directories "Examples"
   971   theories
   982   theories
   972     Types_To_Sets
   983     Types_To_Sets
   973     "Examples/Prerequisites"
   984     "Examples/Prerequisites"
   974     "Examples/Finite"
   985     "Examples/Finite"
   975     "Examples/T2_Spaces"
   986     "Examples/T2_Spaces"