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