src/HOL/ROOT
author blanchet
Thu Sep 11 19:26:59 2014 +0200 (2014-09-11)
changeset 58309 a09ec6daaa19
parent 58308 0ccba1b6d00b
child 58312 710f56e192fe
permissions -rw-r--r--
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
     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     Sudoku
   601     Nominal2_Dummy
   602   theories [skip_proofs = false]
   603     Meson_Test
   604   theories [condition = SVC_HOME]
   605     svc_test
   606   document_files "root.bib" "root.tex"
   607 
   608 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   609   description {*
   610     Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
   611   *}
   612   theories [document = false]
   613     "~~/src/HOL/Library/Lattice_Syntax"
   614     "../Number_Theory/Primes"
   615   theories
   616     Basic_Logic
   617     Cantor
   618     Drinker
   619     Expr_Compiler
   620     Fibonacci
   621     Group
   622     Group_Context
   623     Group_Notepad
   624     Hoare_Ex
   625     Knaster_Tarski
   626     Mutilated_Checkerboard
   627     Nested_Datatype
   628     Peirce
   629     Puzzle
   630     Summation
   631   document_files
   632     "root.bib"
   633     "root.tex"
   634     "style.tex"
   635 
   636 session "HOL-SET_Protocol" in SET_Protocol = HOL +
   637   description {*
   638     Verification of the SET Protocol.
   639   *}
   640   options [document_graph]
   641   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
   642   theories SET_Protocol
   643   document_files "root.tex"
   644 
   645 session "HOL-Matrix_LP" in Matrix_LP = HOL +
   646   description {*
   647     Two-dimensional matrices and linear programming.
   648   *}
   649   options [document_graph]
   650   theories Cplex
   651   document_files "root.tex"
   652 
   653 session "HOL-TLA" in TLA = HOL +
   654   description {*
   655     Lamport's Temporal Logic of Actions.
   656   *}
   657   options [document = false]
   658   theories TLA
   659 
   660 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   661   options [document = false]
   662   theories Inc
   663 
   664 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   665   options [document = false]
   666   theories DBuffer
   667 
   668 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   669   options [document = false]
   670   theories MemoryImplementation
   671 
   672 session "HOL-TPTP" in TPTP = HOL +
   673   description {*
   674     Author:     Jasmin Blanchette, TU Muenchen
   675     Author:     Nik Sultana, University of Cambridge
   676     Copyright   2011
   677 
   678     TPTP-related extensions.
   679   *}
   680   options [document = false]
   681   theories
   682     ATP_Theory_Export
   683     MaSh_Eval
   684     TPTP_Interpret
   685     THF_Arith
   686     TPTP_Proof_Reconstruction
   687   theories
   688     ATP_Problem_Import
   689 
   690 session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +
   691   options [document_graph]
   692   theories
   693     Multivariate_Analysis
   694     Determinants
   695     PolyRoots
   696     Complex_Analysis_Basics
   697   document_files
   698     "root.tex"
   699 
   700 session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
   701   options [document_graph]
   702   theories [document = false]
   703     "~~/src/HOL/Library/Countable"
   704     "~~/src/HOL/Library/Permutation"
   705     "~~/src/HOL/Library/Order_Continuity"
   706     "~~/src/HOL/Library/Diagonal_Subsequence"
   707   theories
   708     Probability
   709     "ex/Dining_Cryptographers"
   710     "ex/Koepf_Duermuth_Countermeasure"
   711   document_files "root.tex"
   712 
   713 session "HOL-Nominal" (main) in Nominal = HOL +
   714   options [document = false]
   715   theories Nominal
   716 
   717 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
   718   options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
   719   theories Nominal_Examples
   720   theories [quick_and_dirty] VC_Condition
   721 
   722 session "HOL-Cardinals" in Cardinals = HOL +
   723   description {*
   724     Ordinals and Cardinals, Full Theories.
   725   *}
   726   options [document = false]
   727   theories Cardinals
   728   document_files
   729     "intro.tex"
   730     "root.tex"
   731     "root.bib"
   732 
   733 session "HOL-Datatype_Examples" in Datatype_Examples = HOL +
   734   description {*
   735     (Co)datatype Examples.
   736   *}
   737   options [document = false]
   738   theories
   739     Compat
   740     Lambda_Term
   741     Process
   742     TreeFsetI
   743     "Derivation_Trees/Gram_Lang"
   744     "Derivation_Trees/Parallel"
   745     Koenig
   746     Stream_Processor
   747     Misc_Codatatype
   748     Misc_Datatype
   749     Misc_Primcorec
   750     Misc_Primrec
   751   theories [condition = ISABELLE_FULL_TEST]
   752     Brackin
   753     Instructions
   754     IsaFoR_Datatypes
   755     SML
   756     Verilog
   757 
   758 session "HOL-Word" (main) in Word = HOL +
   759   options [document_graph]
   760   theories Word
   761   document_files "root.bib" "root.tex"
   762 
   763 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   764   options [document = false]
   765   theories WordExamples
   766 
   767 session "HOL-Statespace" in Statespace = HOL +
   768   theories [skip_proofs = false]
   769     StateSpaceEx
   770   document_files "root.tex"
   771 
   772 session "HOL-NSA" in NSA = HOL +
   773   description {*
   774     Nonstandard analysis.
   775   *}
   776   options [document_graph]
   777   theories Hypercomplex
   778   document_files "root.tex"
   779 
   780 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   781   options [document = false]
   782   theories NSPrimes
   783 
   784 session "HOL-Mirabelle" in Mirabelle = HOL +
   785   options [document = false]
   786   theories Mirabelle_Test
   787 
   788 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   789   options [document = false, timeout = 60]
   790   theories Ex
   791 
   792 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   793   options [document = false, quick_and_dirty]
   794   theories
   795     Boogie
   796     SMT_Examples
   797     SMT_Word_Examples
   798   theories [condition = ISABELLE_FULL_TEST]
   799     SMT_Tests
   800   files
   801     "Boogie_Dijkstra.certs2"
   802     "Boogie_Max.certs2"
   803     "SMT_Examples.certs2"
   804     "SMT_Word_Examples.certs2"
   805     "VCC_Max.certs2"
   806 
   807 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   808   options [document = false]
   809   theories SPARK
   810 
   811 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   812   options [document = false]
   813   theories
   814     "Gcd/Greatest_Common_Divisor"
   815 
   816     "Liseq/Longest_Increasing_Subsequence"
   817 
   818     "RIPEMD-160/F"
   819     "RIPEMD-160/Hash"
   820     "RIPEMD-160/K_L"
   821     "RIPEMD-160/K_R"
   822     "RIPEMD-160/R_L"
   823     "RIPEMD-160/Round"
   824     "RIPEMD-160/R_R"
   825     "RIPEMD-160/S_L"
   826     "RIPEMD-160/S_R"
   827 
   828     "Sqrt/Sqrt"
   829   files
   830     "Gcd/greatest_common_divisor/g_c_d.fdl"
   831     "Gcd/greatest_common_divisor/g_c_d.rls"
   832     "Gcd/greatest_common_divisor/g_c_d.siv"
   833     "Liseq/liseq/liseq_length.fdl"
   834     "Liseq/liseq/liseq_length.rls"
   835     "Liseq/liseq/liseq_length.siv"
   836     "RIPEMD-160/rmd/f.fdl"
   837     "RIPEMD-160/rmd/f.rls"
   838     "RIPEMD-160/rmd/f.siv"
   839     "RIPEMD-160/rmd/hash.fdl"
   840     "RIPEMD-160/rmd/hash.rls"
   841     "RIPEMD-160/rmd/hash.siv"
   842     "RIPEMD-160/rmd/k_l.fdl"
   843     "RIPEMD-160/rmd/k_l.rls"
   844     "RIPEMD-160/rmd/k_l.siv"
   845     "RIPEMD-160/rmd/k_r.fdl"
   846     "RIPEMD-160/rmd/k_r.rls"
   847     "RIPEMD-160/rmd/k_r.siv"
   848     "RIPEMD-160/rmd/r_l.fdl"
   849     "RIPEMD-160/rmd/r_l.rls"
   850     "RIPEMD-160/rmd/r_l.siv"
   851     "RIPEMD-160/rmd/round.fdl"
   852     "RIPEMD-160/rmd/round.rls"
   853     "RIPEMD-160/rmd/round.siv"
   854     "RIPEMD-160/rmd/r_r.fdl"
   855     "RIPEMD-160/rmd/r_r.rls"
   856     "RIPEMD-160/rmd/r_r.siv"
   857     "RIPEMD-160/rmd/s_l.fdl"
   858     "RIPEMD-160/rmd/s_l.rls"
   859     "RIPEMD-160/rmd/s_l.siv"
   860     "RIPEMD-160/rmd/s_r.fdl"
   861     "RIPEMD-160/rmd/s_r.rls"
   862     "RIPEMD-160/rmd/s_r.siv"
   863 
   864 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   865   options [show_question_marks = false]
   866   theories
   867     Example_Verification
   868     VC_Principles
   869     Reference
   870     Complex_Types
   871   files
   872     "complex_types_app/initialize.fdl"
   873     "complex_types_app/initialize.rls"
   874     "complex_types_app/initialize.siv"
   875     "loop_invariant/proc1.fdl"
   876     "loop_invariant/proc1.rls"
   877     "loop_invariant/proc1.siv"
   878     "loop_invariant/proc2.fdl"
   879     "loop_invariant/proc2.rls"
   880     "loop_invariant/proc2.siv"
   881     "simple_greatest_common_divisor/g_c_d.fdl"
   882     "simple_greatest_common_divisor/g_c_d.rls"
   883     "simple_greatest_common_divisor/g_c_d.siv"
   884   document_files
   885     "complex_types.ads"
   886     "complex_types_app.adb"
   887     "complex_types_app.ads"
   888     "Gcd.adb"
   889     "Gcd.ads"
   890     "intro.tex"
   891     "loop_invariant.adb"
   892     "loop_invariant.ads"
   893     "root.bib"
   894     "root.tex"
   895     "Simple_Gcd.adb"
   896     "Simple_Gcd.ads"
   897 
   898 session "HOL-Mutabelle" in Mutabelle = HOL +
   899   options [document = false]
   900   theories MutabelleExtra
   901 
   902 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   903   options [document = false]
   904   theories
   905     Quickcheck_Examples
   906     Quickcheck_Lattice_Examples
   907     Completeness
   908     Quickcheck_Interfaces
   909   theories [condition = ISABELLE_GHC]
   910     Hotel_Example
   911     Quickcheck_Narrowing_Examples
   912 
   913 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   914   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   915     Find_Unused_Assms_Examples
   916     Needham_Schroeder_No_Attacker_Example
   917     Needham_Schroeder_Guided_Attacker_Example
   918     Needham_Schroeder_Unguided_Attacker_Example
   919 
   920 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   921   description {*
   922     Author:     Cezary Kaliszyk and Christian Urban
   923   *}
   924   options [document = false]
   925   theories
   926     DList
   927     FSet
   928     Quotient_Int
   929     Quotient_Message
   930     Lift_FSet
   931     Lift_Set
   932     Lift_Fun
   933     Quotient_Rat
   934     Lift_DList
   935     Int_Pow
   936 
   937 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   938   options [document = false]
   939   theories
   940     Examples
   941     Predicate_Compile_Tests
   942     (* FIXME
   943     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   944     Specialisation_Examples
   945     IMP_1
   946     IMP_2
   947     (* FIXME since 21-Jul-2011
   948     Hotel_Example_Small_Generator
   949     IMP_3
   950     IMP_4 *)
   951   theories [condition = "ISABELLE_SWIPL"]
   952     Code_Prolog_Examples
   953     Context_Free_Grammar_Example
   954     Hotel_Example_Prolog
   955     Lambda_Example
   956     List_Examples
   957   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]
   958     Reg_Exp_Example
   959 
   960 session HOLCF (main) in HOLCF = HOL +
   961   description {*
   962     Author:     Franz Regensburger
   963     Author:     Brian Huffman
   964 
   965     HOLCF -- a semantic extension of HOL by the LCF logic.
   966   *}
   967   options [document_graph]
   968   theories [document = false]
   969     "~~/src/HOL/Library/Nat_Bijection"
   970     "~~/src/HOL/Library/Countable"
   971   theories
   972     Plain_HOLCF
   973     Fixrec
   974     HOLCF
   975   document_files "root.tex"
   976 
   977 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   978   theories
   979     Domain_ex
   980     Fixrec_ex
   981     New_Domain
   982   document_files "root.tex"
   983 
   984 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   985   options [document = false]
   986   theories HOLCF_Library
   987 
   988 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   989   description {*
   990     IMP -- A WHILE-language and its Semantics.
   991 
   992     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   993   *}
   994   options [document = false]
   995   theories HoareEx
   996   document_files "root.tex"
   997 
   998 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   999   description {*
  1000     Miscellaneous examples for HOLCF.
  1001   *}
  1002   options [document = false]
  1003   theories
  1004     Dnat
  1005     Dagstuhl
  1006     Focus_ex
  1007     Fix2
  1008     Hoare
  1009     Concurrency_Monad
  1010     Loop
  1011     Powerdomain_ex
  1012     Domain_Proofs
  1013     Letrec
  1014     Pattern_Match
  1015 
  1016 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
  1017   description {*
  1018     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
  1019 
  1020     For introductions to FOCUS, see
  1021 
  1022     "The Design of Distributed Systems - An Introduction to FOCUS"
  1023     http://www4.in.tum.de/publ/html.php?e=2
  1024 
  1025     "Specification and Refinement of a Buffer of Length One"
  1026     http://www4.in.tum.de/publ/html.php?e=15
  1027 
  1028     "Specification and Development of Interactive Systems: Focus on Streams,
  1029     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1030   *}
  1031   options [document = false]
  1032   theories
  1033     Fstreams
  1034     FOCUS
  1035     Buffer_adm
  1036 
  1037 session IOA in "HOLCF/IOA" = HOLCF +
  1038   description {*
  1039     Author:     Olaf Mueller
  1040     Copyright   1997 TU München
  1041 
  1042     A formalization of I/O automata in HOLCF.
  1043 
  1044     The distribution contains simulation relations, temporal logic, and an
  1045     abstraction theory. Everything is based upon a domain-theoretic model of
  1046     finite and infinite sequences.
  1047   *}
  1048   options [document = false]
  1049   theories "meta_theory/Abstraction"
  1050 
  1051 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1052   description {*
  1053     Author:     Olaf Mueller
  1054 
  1055     The Alternating Bit Protocol performed in I/O-Automata.
  1056   *}
  1057   options [document = false]
  1058   theories Correctness
  1059 
  1060 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1061   description {*
  1062     Author:     Tobias Nipkow & Konrad Slind
  1063 
  1064     A network transmission protocol, performed in the
  1065     I/O automata formalization by Olaf Mueller.
  1066   *}
  1067   options [document = false]
  1068   theories Correctness
  1069 
  1070 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1071   description {*
  1072     Author:     Olaf Mueller
  1073 
  1074     Memory storage case study.
  1075   *}
  1076   options [document = false]
  1077   theories Correctness
  1078 
  1079 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1080   description {*
  1081     Author:     Olaf Mueller
  1082   *}
  1083   options [document = false]
  1084   theories
  1085     TrivEx
  1086     TrivEx2
  1087 
  1088 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
  1089   description {*
  1090     Some rather large datatype examples (from John Harrison).
  1091   *}
  1092   options [document = false]
  1093   theories [condition = ISABELLE_FULL_TEST, timing]
  1094     Brackin
  1095     Instructions
  1096     SML
  1097     Verilog
  1098 
  1099 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
  1100   description {*
  1101     Some benchmark on large record.
  1102   *}
  1103   options [document = false]
  1104   theories [condition = ISABELLE_FULL_TEST, timing]
  1105     Record_Benchmark
  1106