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