src/HOL/ROOT
changeset 65538 a39ef48fbee0
parent 65535 1bf7b5dc34c8
child 65543 8369b33fda0a
equal deleted inserted replaced
65537:7ce5fcebfb35 65538:a39ef48fbee0
   192   theories EvenOdd
   192   theories EvenOdd
   193 
   193 
   194 session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
   194 session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
   195   options [document_variants = document]
   195   options [document_variants = document]
   196   theories [document = false]
   196   theories [document = false]
   197     "Less_False"
   197     Less_False
   198     "~~/src/HOL/Library/Multiset"
   198     "~~/src/HOL/Library/Multiset"
   199     "~~/src/HOL/Number_Theory/Fib"
   199     "~~/src/HOL/Number_Theory/Fib"
   200   theories
   200   theories
   201     Balance
   201     Balance
   202     Tree_Map
   202     Tree_Map
   350 
   350 
   351     Verifying security protocols using Chandy and Misra's UNITY formalism.
   351     Verifying security protocols using Chandy and Misra's UNITY formalism.
   352   *}
   352   *}
   353   theories
   353   theories
   354     (*Basic meta-theory*)
   354     (*Basic meta-theory*)
   355     "UNITY_Main"
   355     UNITY_Main
   356 
   356 
   357     (*Simple examples: no composition*)
   357     (*Simple examples: no composition*)
   358     "Simple/Deadlock"
   358     "Simple/Deadlock"
   359     "Simple/Common"
   359     "Simple/Common"
   360     "Simple/Network"
   360     "Simple/Network"
   382     "Comp/Alloc"
   382     "Comp/Alloc"
   383     "Comp/AllocImpl"
   383     "Comp/AllocImpl"
   384     "Comp/Client"
   384     "Comp/Client"
   385 
   385 
   386     (*obsolete*)
   386     (*obsolete*)
   387     "ELT"
   387     ELT
   388   document_files "root.tex"
   388   document_files "root.tex"
   389 
   389 
   390 session "HOL-Unix" in Unix = HOL +
   390 session "HOL-Unix" in Unix = HOL +
   391   options [print_mode = "no_brackets,no_type_brackets"]
   391   options [print_mode = "no_brackets,no_type_brackets"]
   392   theories Unix
   392   theories Unix
   739     Probability (global)
   739     Probability (global)
   740   document_files "root.tex"
   740   document_files "root.tex"
   741 
   741 
   742 session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
   742 session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
   743   theories
   743   theories
   744     "Dining_Cryptographers"
   744     Dining_Cryptographers
   745     "Koepf_Duermuth_Countermeasure"
   745     Koepf_Duermuth_Countermeasure
   746     "Measure_Not_CCC"
   746     Measure_Not_CCC
   747 
   747 
   748 session "HOL-Nominal" in Nominal = HOL +
   748 session "HOL-Nominal" in Nominal = HOL +
   749   options [document = false]
   749   options [document = false]
   750   theories Nominal
   750   theories Nominal
   751 
   751 
  1122     The distribution contains simulation relations, temporal logic, and an
  1122     The distribution contains simulation relations, temporal logic, and an
  1123     abstraction theory. Everything is based upon a domain-theoretic model of
  1123     abstraction theory. Everything is based upon a domain-theoretic model of
  1124     finite and infinite sequences.
  1124     finite and infinite sequences.
  1125   *}
  1125   *}
  1126   options [document = false]
  1126   options [document = false]
  1127   theories "Abstraction"
  1127   theories Abstraction
  1128 
  1128 
  1129 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1129 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1130   description {*
  1130   description {*
  1131     Author:     Olaf Mueller
  1131     Author:     Olaf Mueller
  1132 
  1132