src/HOL/ROOT
author blanchet
Thu Sep 18 00:03:46 2014 +0200 (2014-09-18)
changeset 58367 8af1e68d7e1a
parent 58351 b3f7c69e9fcd
child 58371 7f30ec82fe40
permissions -rw-r--r--
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
     1 chapter HOL
     2 
     3 session HOL (main) = Pure +
     4   description {*
     5     Classical Higher-order Logic.
     6   *}
     7   options [document_graph]
     8   global_theories
     9     Main
    10     Complex_Main
    11   files
    12     "Tools/Quickcheck/Narrowing_Engine.hs"
    13     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    14   document_files
    15     "root.bib"
    16     "root.tex"
    17 
    18 session "HOL-Proofs" = Pure +
    19   description {*
    20     HOL-Main with explicit proof terms.
    21   *}
    22   options [document = false]
    23   theories Proofs (*sequential change of global flag!*)
    24   theories Main
    25   files
    26     "Tools/Quickcheck/Narrowing_Engine.hs"
    27     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
    28 
    29 session "HOL-Library" (main) in Library = HOL +
    30   description {*
    31     Classical Higher-order Logic -- batteries included.
    32   *}
    33   theories
    34     Library
    35     (*conflicting type class instantiations*)
    36     List_lexord
    37     Sublist_Order
    38     Product_Lexorder
    39     Product_Order
    40     Finite_Lattice
    41     (*data refinements and dependent applications*)
    42     AList_Mapping
    43     Code_Binary_Nat
    44     Code_Char
    45     Code_Prolog
    46     Code_Real_Approx_By_Float
    47     Code_Target_Numeral
    48     DAList
    49     DAList_Multiset
    50     RBT_Mapping
    51     RBT_Set
    52     (*legacy tools*)
    53     Refute
    54     Old_Recdef
    55     Old_SMT
    56   theories [condition = ISABELLE_FULL_TEST]
    57     Sum_of_Squares_Remote
    58   document_files "root.bib" "root.tex"
    59 
    60 session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
    61   description {*
    62     Author:     Gertrud Bauer, TU Munich
    63 
    64     The Hahn-Banach theorem for real vector spaces.
    65 
    66     This is the proof of the Hahn-Banach theorem for real vectorspaces,
    67     following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach
    68     theorem is one of the fundamental theorems of functional analysis. It is a
    69     conclusion of Zorn's lemma.
    70 
    71     Two different formaulations of the theorem are presented, one for general
    72     real vectorspaces and its application to normed vectorspaces.
    73 
    74     The theorem says, that every continous linearform, defined on arbitrary
    75     subspaces (not only one-dimensional subspaces), can be extended to a
    76     continous linearform on the whole vectorspace.
    77   *}
    78   options [document_graph]
    79   theories Hahn_Banach
    80   document_files "root.bib" "root.tex"
    81 
    82 session "HOL-Induct" in Induct = HOL +
    83   description {*
    84     Examples of (Co)Inductive Definitions.
    85 
    86     Comb proves the Church-Rosser theorem for combinators (see
    87     http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz).
    88 
    89     Mutil is the famous Mutilated Chess Board problem (see
    90     http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz).
    91 
    92     PropLog proves the completeness of a formalization of propositional logic
    93     (see
    94     HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
    95 
    96     Exp demonstrates the use of iterated inductive definitions to reason about
    97     mutually recursive relations.
    98   *}
    99   theories [quick_and_dirty]
   100     Common_Patterns
   101   theories
   102     QuoDataType
   103     QuoNestedDataType
   104     Term
   105     SList
   106     ABexp
   107     Tree
   108     Ordinals
   109     Sigma_Algebra
   110     Comb
   111     PropLog
   112     Com
   113   document_files "root.tex"
   114 
   115 session "HOL-IMP" in IMP = HOL +
   116   options [document_graph, document_variants=document]
   117   theories [document = false]
   118     "~~/src/Tools/Permanent_Interpretation"
   119     "~~/src/HOL/Library/While_Combinator"
   120     "~~/src/HOL/Library/Char_ord"
   121     "~~/src/HOL/Library/List_lexord"
   122     "~~/src/HOL/Library/Quotient_List"
   123     "~~/src/HOL/Library/Extended"
   124   theories
   125     BExp
   126     ASM
   127     Finite_Reachable
   128     Denotational
   129     Compiler2
   130     Poly_Types
   131     Sec_Typing
   132     Sec_TypingT
   133     Def_Init_Big
   134     Def_Init_Small
   135     Fold
   136     Live
   137     Live_True
   138     Hoare_Examples
   139     VCG
   140     Hoare_Total
   141     Collecting1
   142     Collecting_Examples
   143     Abs_Int_Tests
   144     Abs_Int1_parity
   145     Abs_Int1_const
   146     Abs_Int3
   147     "Abs_Int_ITP/Abs_Int1_parity_ITP"
   148     "Abs_Int_ITP/Abs_Int1_const_ITP"
   149     "Abs_Int_ITP/Abs_Int3_ITP"
   150     "Abs_Int_Den/Abs_Int_den2"
   151     Procs_Dyn_Vars_Dyn
   152     Procs_Stat_Vars_Dyn
   153     Procs_Stat_Vars_Stat
   154     C_like
   155     OO
   156   document_files "root.bib" "root.tex"
   157 
   158 session "HOL-IMPP" in IMPP = HOL +
   159   description {*
   160     Author:     David von Oheimb
   161     Copyright   1999 TUM
   162 
   163     IMPP -- An imperative language with procedures.
   164 
   165     This is an extension of IMP with local variables and mutually recursive
   166     procedures. For documentation see "Hoare Logic for Mutual Recursion and
   167     Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
   168   *}
   169   options [document = false]
   170   theories EvenOdd
   171 
   172 session "HOL-Import" in Import = HOL +
   173   options [document_graph]
   174   theories HOL_Light_Maps
   175   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
   176 
   177 session "HOL-Number_Theory" in Number_Theory = HOL +
   178   description {*
   179     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
   180     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
   181   *}
   182   options [document_graph]
   183   theories [document = false]
   184     "~~/src/HOL/Library/FuncSet"
   185     "~~/src/HOL/Library/Multiset"
   186     "~~/src/HOL/Algebra/Ring"
   187     "~~/src/HOL/Algebra/FiniteProduct"
   188   theories
   189     Pocklington
   190     Gauss
   191     Number_Theory
   192     Euclidean_Algorithm
   193   document_files
   194     "root.tex"
   195 
   196 session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
   197   description {*
   198     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
   199     Theorem, Wilson's Theorem, Quadratic Reciprocity.
   200   *}
   201   options [document_graph]
   202   theories [document = false]
   203     "~~/src/HOL/Library/Infinite_Set"
   204     "~~/src/HOL/Library/Permutation"
   205   theories
   206     Fib
   207     Factorization
   208     Chinese
   209     WilsonRuss
   210     WilsonBij
   211     Quadratic_Reciprocity
   212     Primes
   213     Pocklington
   214   document_files "root.tex"
   215 
   216 session "HOL-Hoare" in Hoare = HOL +
   217   description {*
   218     Verification of imperative programs (verification conditions are generated
   219     automatically from pre/post conditions and loop invariants).
   220   *}
   221   theories Hoare
   222   document_files "root.bib" "root.tex"
   223 
   224 session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +
   225   description {*
   226     Verification of shared-variable imperative programs a la Owicki-Gries.
   227     (verification conditions are generated automatically).
   228   *}
   229   options [document_graph]
   230   theories Hoare_Parallel
   231   document_files "root.bib" "root.tex"
   232 
   233 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   234   options [document = false, document_graph = false, browser_info = false]
   235   theories
   236     Generate
   237     Generate_Binary_Nat
   238     Generate_Target_Nat
   239     Generate_Efficient_Datastructures
   240     Generate_Pretty_Char
   241     Code_Test
   242   theories[condition = ISABELLE_GHC]
   243     Code_Test_GHC
   244   theories[condition = ISABELLE_MLTON]
   245     Code_Test_MLton
   246   theories[condition = ISABELLE_OCAMLC]
   247     Code_Test_OCaml
   248   theories[condition = ISABELLE_POLYML_PATH]
   249     Code_Test_PolyML
   250   theories[condition = ISABELLE_SCALA]
   251     Code_Test_Scala
   252   theories[condition = ISABELLE_SMLNJ]
   253     Code_Test_SMLNJ
   254 
   255 session "HOL-Metis_Examples" in Metis_Examples = HOL +
   256   description {*
   257     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   258     Author:     Jasmin Blanchette, TU Muenchen
   259 
   260     Testing Metis and Sledgehammer.
   261   *}
   262   options [timeout = 3600, document = false]
   263   theories
   264     Abstraction
   265     Big_O
   266     Binary_Tree
   267     Clausification
   268     Message
   269     Proxies
   270     Tarski
   271     Trans_Closure
   272     Sets
   273 
   274 session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
   275   description {*
   276     Author:     Jasmin Blanchette, TU Muenchen
   277     Copyright   2009
   278   *}
   279   options [document = false]
   280   theories [quick_and_dirty] Nitpick_Examples
   281 
   282 session "HOL-Algebra" (main) in Algebra = HOL +
   283   description {*
   284     Author: Clemens Ballarin, started 24 September 1999
   285 
   286     The Isabelle Algebraic Library.
   287   *}
   288   options [document_graph]
   289   theories [document = false]
   290     (* Preliminaries from set and number theory *)
   291     "~~/src/HOL/Library/FuncSet"
   292     "~~/src/HOL/Number_Theory/Primes"
   293     "~~/src/HOL/Number_Theory/Binomial"
   294     "~~/src/HOL/Library/Permutation"
   295   theories
   296     (*** New development, based on explicit structures ***)
   297     (* Groups *)
   298     FiniteProduct        (* Product operator for commutative groups *)
   299     Sylow                (* Sylow's theorem *)
   300     Bij                  (* Automorphism Groups *)
   301 
   302     (* Rings *)
   303     Divisibility         (* Rings *)
   304     IntRing              (* Ideals and residue classes *)
   305     UnivPoly             (* Polynomials *)
   306   document_files "root.bib" "root.tex"
   307 
   308 session "HOL-Auth" in Auth = HOL +
   309   description {*
   310     A new approach to verifying authentication protocols.
   311   *}
   312   options [document_graph]
   313   theories
   314     Auth_Shared
   315     Auth_Public
   316     "Smartcard/Auth_Smartcard"
   317     "Guard/Auth_Guard_Shared"
   318     "Guard/Auth_Guard_Public"
   319   document_files "root.tex"
   320 
   321 session "HOL-UNITY" in UNITY = "HOL-Auth" +
   322   description {*
   323     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   324     Copyright   1998  University of Cambridge
   325 
   326     Verifying security protocols using Chandy and Misra's UNITY formalism.
   327   *}
   328   options [document_graph]
   329   theories
   330     (*Basic meta-theory*)
   331     "UNITY_Main"
   332 
   333     (*Simple examples: no composition*)
   334     "Simple/Deadlock"
   335     "Simple/Common"
   336     "Simple/Network"
   337     "Simple/Token"
   338     "Simple/Channel"
   339     "Simple/Lift"
   340     "Simple/Mutex"
   341     "Simple/Reach"
   342     "Simple/Reachability"
   343 
   344     (*Verifying security protocols using UNITY*)
   345     "Simple/NSP_Bad"
   346 
   347     (*Example of composition*)
   348     "Comp/Handshake"
   349 
   350     (*Universal properties examples*)
   351     "Comp/Counter"
   352     "Comp/Counterc"
   353     "Comp/Priority"
   354 
   355     "Comp/TimerArray"
   356     "Comp/Progress"
   357 
   358     "Comp/Alloc"
   359     "Comp/AllocImpl"
   360     "Comp/Client"
   361 
   362     (*obsolete*)
   363     "ELT"
   364   document_files "root.tex"
   365 
   366 session "HOL-Unix" in Unix = HOL +
   367   options [print_mode = "no_brackets,no_type_brackets"]
   368   theories Unix
   369   document_files "root.bib" "root.tex"
   370 
   371 session "HOL-ZF" in ZF = HOL +
   372   theories MainZF Games
   373   document_files "root.tex"
   374 
   375 session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
   376   options [document_graph, print_mode = "iff,no_brackets"]
   377   theories [document = false]
   378     "~~/src/HOL/Library/Countable"
   379     "~~/src/HOL/Library/Monad_Syntax"
   380     "~~/src/HOL/Library/LaTeXsugar"
   381   theories Imperative_HOL_ex
   382   document_files "root.bib" "root.tex"
   383 
   384 session "HOL-Decision_Procs" in Decision_Procs = HOL +
   385   description {*
   386     Various decision procedures, typically involving reflection.
   387   *}
   388   options [condition = ISABELLE_POLYML, document = false]
   389   theories Decision_Procs
   390 
   391 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   392   options [document = false, parallel_proofs = 0]
   393   theories
   394     Hilbert_Classical
   395     XML_Data
   396 
   397 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
   398   description {*
   399     Examples for program extraction in Higher-Order Logic.
   400   *}
   401   options [condition = ISABELLE_POLYML, parallel_proofs = 0]
   402   theories [document = false]
   403     "~~/src/HOL/Library/Code_Target_Numeral"
   404     "~~/src/HOL/Library/Monad_Syntax"
   405     "~~/src/HOL/Number_Theory/Primes"
   406     "~~/src/HOL/Number_Theory/UniqueFactorization"
   407     "~~/src/HOL/Library/State_Monad"
   408   theories
   409     Greatest_Common_Divisor
   410     Warshall
   411     Higman_Extraction
   412     Pigeonhole
   413     Euclid
   414   document_files "root.bib" "root.tex"
   415 
   416 session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
   417   description {*
   418     Lambda Calculus in de Bruijn's Notation.
   419 
   420     This session defines lambda-calculus terms with de Bruijn indixes and
   421     proves confluence of beta, eta and beta+eta.
   422 
   423     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
   424     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   425   *}
   426   options [document_graph, print_mode = "no_brackets", parallel_proofs = 0]
   427   theories [document = false]
   428     "~~/src/HOL/Library/Code_Target_Int"
   429   theories
   430     Eta
   431     StrongNorm
   432     Standardization
   433     WeakNorm
   434   document_files "root.bib" "root.tex"
   435 
   436 session "HOL-Prolog" in Prolog = HOL +
   437   description {*
   438     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
   439 
   440     A bare-bones implementation of Lambda-Prolog.
   441 
   442     This is a simple exploratory implementation of Lambda-Prolog in HOL,
   443     including some minimal examples (in Test.thy) and a more typical example of
   444     a little functional language and its type system.
   445   *}
   446   options [document = false]
   447   theories Test Type
   448 
   449 session "HOL-MicroJava" in MicroJava = HOL +
   450   description {*
   451     Formalization of a fragment of Java, together with a corresponding virtual
   452     machine and a specification of its bytecode verifier and a lightweight
   453     bytecode verifier, including proofs of type-safety.
   454   *}
   455   options [document_graph]
   456   theories [document = false] "~~/src/HOL/Library/While_Combinator"
   457   theories MicroJava
   458   document_files
   459     "introduction.tex"
   460     "root.bib"
   461     "root.tex"
   462 
   463 session "HOL-NanoJava" in NanoJava = HOL +
   464   description {*
   465     Hoare Logic for a tiny fragment of Java.
   466   *}
   467   options [document_graph]
   468   theories Example
   469   document_files "root.bib" "root.tex"
   470 
   471 session "HOL-Bali" in Bali = HOL +
   472   options [document_graph]
   473   theories
   474     AxExample
   475     AxSound
   476     AxCompl
   477     Trans
   478   document_files "root.tex"
   479 
   480 session "HOL-IOA" in IOA = HOL +
   481   description {*
   482     Author:     Tobias Nipkow and Konrad Slind and Olaf Müller
   483     Copyright   1994--1996  TU Muenchen
   484 
   485     The meta-theory of I/O-Automata in HOL. This formalization has been
   486     significantly changed and extended, see HOLCF/IOA. There are also the
   487     proofs of two communication protocols which formerly have been here.
   488 
   489     @inproceedings{Nipkow-Slind-IOA,
   490     author={Tobias Nipkow and Konrad Slind},
   491     title={{I/O} Automata in {Isabelle/HOL}},
   492     booktitle={Proc.\ TYPES Workshop 1994},
   493     publisher=Springer,
   494     series=LNCS,
   495     note={To appear}}
   496     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
   497 
   498     and
   499 
   500     @inproceedings{Mueller-Nipkow,
   501     author={Olaf M\"uller and Tobias Nipkow},
   502     title={Combining Model Checking and Deduction for {I/O}-Automata},
   503     booktitle={Proc.\ TACAS Workshop},
   504     organization={Aarhus University, BRICS report},
   505     year=1995}
   506     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   507   *}
   508   options [document = false]
   509   theories Solve
   510 
   511 session "HOL-Lattice" in Lattice = HOL +
   512   description {*
   513     Author:     Markus Wenzel, TU Muenchen
   514 
   515     Basic theory of lattices and orders.
   516   *}
   517   theories CompleteLattice
   518   document_files "root.tex"
   519 
   520 session "HOL-ex" in ex = HOL +
   521   description {*
   522     Miscellaneous examples for Higher-Order Logic.
   523   *}
   524   options [timeout = 3600, condition = ISABELLE_POLYML]
   525   theories [document = false]
   526     "~~/src/HOL/Library/State_Monad"
   527     Code_Binary_Nat_examples
   528     "~~/src/HOL/Library/FuncSet"
   529     Eval_Examples
   530     Normalization_by_Evaluation
   531     Hebrew
   532     Chinese
   533     Serbian
   534     "~~/src/HOL/Library/FinFun_Syntax"
   535     "~~/src/HOL/Library/Refute"
   536     "~~/src/HOL/Library/Transitive_Closure_Table"
   537     Cartouche_Examples
   538   theories
   539     Adhoc_Overloading_Examples
   540     Iff_Oracle
   541     Coercion_Examples
   542     Higher_Order_Logic
   543     Abstract_NAT
   544     Guess
   545     Fundefs
   546     Induction_Schema
   547     LocaleTest2
   548     Records
   549     While_Combinator_Example
   550     MonoidGroup
   551     BinEx
   552     Hex_Bin_Examples
   553     Antiquote
   554     Multiquote
   555     PER
   556     NatSum
   557     ThreeDivides
   558     Intuitionistic
   559     CTL
   560     Arith_Examples
   561     BT
   562     Tree23
   563     MergeSort
   564     Lagrange
   565     Groebner_Examples
   566     MT
   567     Unification
   568     Primrec
   569     Tarski
   570     Classical
   571     Set_Theory
   572     Termination
   573     Coherent
   574     PresburgerEx
   575     Reflection_Examples
   576     Sqrt
   577     Sqrt_Script
   578     Transfer_Ex
   579     Transfer_Int_Nat
   580     Transitive_Closure_Table_Ex
   581     HarmonicSeries
   582     Refute_Examples
   583     Execute_Choice
   584     Gauge_Integration
   585     Dedekind_Real
   586     Quicksort
   587     Birthday_Paradox
   588     List_to_Set_Comprehension_Examples
   589     Seq
   590     Simproc_Tests
   591     Executable_Relation
   592     FinFunPred
   593     Set_Comprehension_Pointfree_Examples
   594     Parallel_Example
   595     IArray_Examples
   596     SVC_Oracle
   597     Simps_Case_Conv_Examples
   598     ML
   599     SAT_Examples
   600     Nominal2_Dummy
   601   theories [skip_proofs = false]
   602     Meson_Test
   603   theories [condition = SVC_HOME]
   604     svc_test
   605   theories [condition = ISABELLE_FULL_TEST]
   606     Sudoku
   607   document_files "root.bib" "root.tex"
   608 
   609 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   610   description {*
   611     Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
   612   *}
   613   theories [document = false]
   614     "~~/src/HOL/Library/Lattice_Syntax"
   615     "../Number_Theory/Primes"
   616   theories
   617     Basic_Logic
   618     Cantor
   619     Drinker
   620     Expr_Compiler
   621     Fibonacci
   622     Group
   623     Group_Context
   624     Group_Notepad
   625     Hoare_Ex
   626     Knaster_Tarski
   627     Mutilated_Checkerboard
   628     Nested_Datatype
   629     Peirce
   630     Puzzle
   631     Summation
   632   document_files
   633     "root.bib"
   634     "root.tex"
   635     "style.tex"
   636 
   637 session "HOL-SET_Protocol" in SET_Protocol = HOL +
   638   description {*
   639     Verification of the SET Protocol.
   640   *}
   641   options [document_graph]
   642   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   643   theories SET_Protocol
   644   document_files "root.tex"
   645 
   646 session "HOL-Matrix_LP" in Matrix_LP = HOL +
   647   description {*
   648     Two-dimensional matrices and linear programming.
   649   *}
   650   options [document_graph]
   651   theories Cplex
   652   document_files "root.tex"
   653 
   654 session "HOL-TLA" in TLA = HOL +
   655   description {*
   656     Lamport's Temporal Logic of Actions.
   657   *}
   658   options [document = false]
   659   theories TLA
   660 
   661 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   662   options [document = false]
   663   theories Inc
   664 
   665 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   666   options [document = false]
   667   theories DBuffer
   668 
   669 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   670   options [document = false]
   671   theories MemoryImplementation
   672 
   673 session "HOL-TPTP" in TPTP = HOL +
   674   description {*
   675     Author:     Jasmin Blanchette, TU Muenchen
   676     Author:     Nik Sultana, University of Cambridge
   677     Copyright   2011
   678 
   679     TPTP-related extensions.
   680   *}
   681   options [document = false]
   682   theories
   683     ATP_Theory_Export
   684     MaSh_Eval
   685     TPTP_Interpret
   686     THF_Arith
   687     TPTP_Proof_Reconstruction
   688   theories
   689     ATP_Problem_Import
   690 
   691 session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
   692   options [document_graph]
   693   theories
   694     Multivariate_Analysis
   695     Determinants
   696     PolyRoots
   697     Complex_Analysis_Basics
   698   document_files
   699     "root.tex"
   700 
   701 session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   702   options [document_graph]
   703   theories [document = false]
   704     "~~/src/HOL/Library/Countable"
   705     "~~/src/HOL/Library/Permutation"
   706     "~~/src/HOL/Library/Order_Continuity"
   707     "~~/src/HOL/Library/Diagonal_Subsequence"
   708   theories
   709     Probability
   710     "ex/Dining_Cryptographers"
   711     "ex/Koepf_Duermuth_Countermeasure"
   712   document_files "root.tex"
   713 
   714 session "HOL-Nominal" (main) in Nominal = HOL +
   715   options [document = false]
   716   theories Nominal
   717 
   718 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   719   options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
   720   theories
   721     Nominal_Examples_Base
   722   theories [condition = ISABELLE_FULL_TEST]
   723     Nominal_Examples
   724   theories [quick_and_dirty]
   725     VC_Condition
   726 
   727 session "HOL-Cardinals" in Cardinals = HOL +
   728   description {*
   729     Ordinals and Cardinals, Full Theories.
   730   *}
   731   options [document = false]
   732   theories Cardinals
   733   document_files
   734     "intro.tex"
   735     "root.tex"
   736     "root.bib"
   737 
   738 session "HOL-Datatype_Examples" in Datatype_Examples = HOL +
   739   description {*
   740     (Co)datatype Examples, including large ones from John Harrison.
   741   *}
   742   options [document = false]
   743   theories
   744     Compat
   745     Lambda_Term
   746     Process
   747     TreeFsetI
   748     "Derivation_Trees/Gram_Lang"
   749     "Derivation_Trees/Parallel"
   750     Koenig
   751     Stream_Processor
   752     Misc_Codatatype
   753     Misc_Datatype
   754     Misc_Primcorec
   755     Misc_Primrec
   756   theories [condition = ISABELLE_FULL_TEST, timing]
   757     Brackin
   758     IsaFoR
   759 
   760 session "HOL-Word" (main) in Word = HOL +
   761   options [document_graph]
   762   theories Word
   763   document_files "root.bib" "root.tex"
   764 
   765 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   766   options [document = false]
   767   theories WordExamples
   768 
   769 session "HOL-Statespace" in Statespace = HOL +
   770   theories [skip_proofs = false]
   771     StateSpaceEx
   772   document_files "root.tex"
   773 
   774 session "HOL-NSA" in NSA = HOL +
   775   description {*
   776     Nonstandard analysis.
   777   *}
   778   options [document_graph]
   779   theories Hypercomplex
   780   document_files "root.tex"
   781 
   782 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   783   options [document = false]
   784   theories NSPrimes
   785 
   786 session "HOL-Mirabelle" in Mirabelle = HOL +
   787   options [document = false]
   788   theories Mirabelle_Test
   789 
   790 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   791   options [document = false, timeout = 60]
   792   theories Ex
   793 
   794 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   795   options [document = false, quick_and_dirty]
   796   theories
   797     Boogie
   798     SMT_Examples
   799     SMT_Word_Examples
   800   theories [condition = ISABELLE_FULL_TEST]
   801     SMT_Tests
   802   files
   803     "Boogie_Dijkstra.certs"
   804     "Boogie_Max.certs"
   805     "SMT_Examples.certs"
   806     "SMT_Word_Examples.certs"
   807     "VCC_Max.certs"
   808 
   809 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   810   options [document = false]
   811   theories SPARK
   812 
   813 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   814   options [document = false]
   815   theories
   816     "Gcd/Greatest_Common_Divisor"
   817 
   818     "Liseq/Longest_Increasing_Subsequence"
   819 
   820     "RIPEMD-160/F"
   821     "RIPEMD-160/Hash"
   822     "RIPEMD-160/K_L"
   823     "RIPEMD-160/K_R"
   824     "RIPEMD-160/R_L"
   825     "RIPEMD-160/Round"
   826     "RIPEMD-160/R_R"
   827     "RIPEMD-160/S_L"
   828     "RIPEMD-160/S_R"
   829 
   830     "Sqrt/Sqrt"
   831   files
   832     "Gcd/greatest_common_divisor/g_c_d.fdl"
   833     "Gcd/greatest_common_divisor/g_c_d.rls"
   834     "Gcd/greatest_common_divisor/g_c_d.siv"
   835     "Liseq/liseq/liseq_length.fdl"
   836     "Liseq/liseq/liseq_length.rls"
   837     "Liseq/liseq/liseq_length.siv"
   838     "RIPEMD-160/rmd/f.fdl"
   839     "RIPEMD-160/rmd/f.rls"
   840     "RIPEMD-160/rmd/f.siv"
   841     "RIPEMD-160/rmd/hash.fdl"
   842     "RIPEMD-160/rmd/hash.rls"
   843     "RIPEMD-160/rmd/hash.siv"
   844     "RIPEMD-160/rmd/k_l.fdl"
   845     "RIPEMD-160/rmd/k_l.rls"
   846     "RIPEMD-160/rmd/k_l.siv"
   847     "RIPEMD-160/rmd/k_r.fdl"
   848     "RIPEMD-160/rmd/k_r.rls"
   849     "RIPEMD-160/rmd/k_r.siv"
   850     "RIPEMD-160/rmd/r_l.fdl"
   851     "RIPEMD-160/rmd/r_l.rls"
   852     "RIPEMD-160/rmd/r_l.siv"
   853     "RIPEMD-160/rmd/round.fdl"
   854     "RIPEMD-160/rmd/round.rls"
   855     "RIPEMD-160/rmd/round.siv"
   856     "RIPEMD-160/rmd/r_r.fdl"
   857     "RIPEMD-160/rmd/r_r.rls"
   858     "RIPEMD-160/rmd/r_r.siv"
   859     "RIPEMD-160/rmd/s_l.fdl"
   860     "RIPEMD-160/rmd/s_l.rls"
   861     "RIPEMD-160/rmd/s_l.siv"
   862     "RIPEMD-160/rmd/s_r.fdl"
   863     "RIPEMD-160/rmd/s_r.rls"
   864     "RIPEMD-160/rmd/s_r.siv"
   865 
   866 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   867   options [show_question_marks = false]
   868   theories
   869     Example_Verification
   870     VC_Principles
   871     Reference
   872     Complex_Types
   873   files
   874     "complex_types_app/initialize.fdl"
   875     "complex_types_app/initialize.rls"
   876     "complex_types_app/initialize.siv"
   877     "loop_invariant/proc1.fdl"
   878     "loop_invariant/proc1.rls"
   879     "loop_invariant/proc1.siv"
   880     "loop_invariant/proc2.fdl"
   881     "loop_invariant/proc2.rls"
   882     "loop_invariant/proc2.siv"
   883     "simple_greatest_common_divisor/g_c_d.fdl"
   884     "simple_greatest_common_divisor/g_c_d.rls"
   885     "simple_greatest_common_divisor/g_c_d.siv"
   886   document_files
   887     "complex_types.ads"
   888     "complex_types_app.adb"
   889     "complex_types_app.ads"
   890     "Gcd.adb"
   891     "Gcd.ads"
   892     "intro.tex"
   893     "loop_invariant.adb"
   894     "loop_invariant.ads"
   895     "root.bib"
   896     "root.tex"
   897     "Simple_Gcd.adb"
   898     "Simple_Gcd.ads"
   899 
   900 session "HOL-Mutabelle" in Mutabelle = HOL +
   901   options [document = false]
   902   theories MutabelleExtra
   903 
   904 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   905   options [document = false]
   906   theories
   907     Quickcheck_Examples
   908     Quickcheck_Lattice_Examples
   909     Completeness
   910     Quickcheck_Interfaces
   911   theories [condition = ISABELLE_GHC]
   912     Hotel_Example
   913     Quickcheck_Narrowing_Examples
   914 
   915 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   916   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   917     Find_Unused_Assms_Examples
   918     Needham_Schroeder_No_Attacker_Example
   919     Needham_Schroeder_Guided_Attacker_Example
   920     Needham_Schroeder_Unguided_Attacker_Example
   921 
   922 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   923   description {*
   924     Author:     Cezary Kaliszyk and Christian Urban
   925   *}
   926   options [document = false]
   927   theories
   928     DList
   929     FSet
   930     Quotient_Int
   931     Quotient_Message
   932     Lift_FSet
   933     Lift_Set
   934     Lift_Fun
   935     Quotient_Rat
   936     Lift_DList
   937     Int_Pow
   938 
   939 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   940   options [document = false]
   941   theories
   942     Examples
   943     Predicate_Compile_Tests
   944     (* FIXME
   945     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   946     Specialisation_Examples
   947     IMP_1
   948     IMP_2
   949     (* FIXME since 21-Jul-2011
   950     Hotel_Example_Small_Generator
   951     IMP_3
   952     IMP_4 *)
   953   theories [condition = "ISABELLE_SWIPL"]
   954     Code_Prolog_Examples
   955     Context_Free_Grammar_Example
   956     Hotel_Example_Prolog
   957     Lambda_Example
   958     List_Examples
   959   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]
   960     Reg_Exp_Example
   961 
   962 session HOLCF (main) in HOLCF = HOL +
   963   description {*
   964     Author:     Franz Regensburger
   965     Author:     Brian Huffman
   966 
   967     HOLCF -- a semantic extension of HOL by the LCF logic.
   968   *}
   969   options [document_graph]
   970   theories [document = false]
   971     "~~/src/HOL/Library/Nat_Bijection"
   972     "~~/src/HOL/Library/Countable"
   973   theories
   974     Plain_HOLCF
   975     Fixrec
   976     HOLCF
   977   document_files "root.tex"
   978 
   979 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   980   theories
   981     Domain_ex
   982     Fixrec_ex
   983     New_Domain
   984   document_files "root.tex"
   985 
   986 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   987   options [document = false]
   988   theories HOLCF_Library
   989 
   990 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   991   description {*
   992     IMP -- A WHILE-language and its Semantics.
   993 
   994     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   995   *}
   996   options [document = false]
   997   theories HoareEx
   998   document_files "root.tex"
   999 
  1000 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
  1001   description {*
  1002     Miscellaneous examples for HOLCF.
  1003   *}
  1004   options [document = false]
  1005   theories
  1006     Dnat
  1007     Dagstuhl
  1008     Focus_ex
  1009     Fix2
  1010     Hoare
  1011     Concurrency_Monad
  1012     Loop
  1013     Powerdomain_ex
  1014     Domain_Proofs
  1015     Letrec
  1016     Pattern_Match
  1017 
  1018 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
  1019   description {*
  1020     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
  1021 
  1022     For introductions to FOCUS, see
  1023 
  1024     "The Design of Distributed Systems - An Introduction to FOCUS"
  1025     http://www4.in.tum.de/publ/html.php?e=2
  1026 
  1027     "Specification and Refinement of a Buffer of Length One"
  1028     http://www4.in.tum.de/publ/html.php?e=15
  1029 
  1030     "Specification and Development of Interactive Systems: Focus on Streams,
  1031     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1032   *}
  1033   options [document = false]
  1034   theories
  1035     Fstreams
  1036     FOCUS
  1037     Buffer_adm
  1038 
  1039 session IOA in "HOLCF/IOA" = HOLCF +
  1040   description {*
  1041     Author:     Olaf Mueller
  1042     Copyright   1997 TU München
  1043 
  1044     A formalization of I/O automata in HOLCF.
  1045 
  1046     The distribution contains simulation relations, temporal logic, and an
  1047     abstraction theory. Everything is based upon a domain-theoretic model of
  1048     finite and infinite sequences.
  1049   *}
  1050   options [document = false]
  1051   theories "meta_theory/Abstraction"
  1052 
  1053 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1054   description {*
  1055     Author:     Olaf Mueller
  1056 
  1057     The Alternating Bit Protocol performed in I/O-Automata.
  1058   *}
  1059   options [document = false]
  1060   theories Correctness
  1061 
  1062 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1063   description {*
  1064     Author:     Tobias Nipkow & Konrad Slind
  1065 
  1066     A network transmission protocol, performed in the
  1067     I/O automata formalization by Olaf Mueller.
  1068   *}
  1069   options [document = false]
  1070   theories Correctness
  1071 
  1072 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1073   description {*
  1074     Author:     Olaf Mueller
  1075 
  1076     Memory storage case study.
  1077   *}
  1078   options [document = false]
  1079   theories Correctness
  1080 
  1081 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1082   description {*
  1083     Author:     Olaf Mueller
  1084   *}
  1085   options [document = false]
  1086   theories
  1087     TrivEx
  1088     TrivEx2
  1089 
  1090 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
  1091   description {*
  1092     Some benchmark on large record.
  1093   *}
  1094   options [document = false]
  1095   theories [condition = ISABELLE_FULL_TEST, timing]
  1096     Record_Benchmark
  1097