src/HOL/ROOT
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 58110 019c0211ed1f
child 58308 0ccba1b6d00b
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     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-BNF_Examples" in BNF_Examples = HOL +
   734   description {*
   735     Examples for Bounded Natural Functors.
   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     IsaFoR_Datatypes
   753 
   754 session "HOL-Word" (main) in Word = HOL +
   755   options [document_graph]
   756   theories Word
   757   document_files "root.bib" "root.tex"
   758 
   759 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
   760   options [document = false]
   761   theories WordExamples
   762 
   763 session "HOL-Statespace" in Statespace = HOL +
   764   theories [skip_proofs = false]
   765     StateSpaceEx
   766   document_files "root.tex"
   767 
   768 session "HOL-NSA" in NSA = HOL +
   769   description {*
   770     Nonstandard analysis.
   771   *}
   772   options [document_graph]
   773   theories Hypercomplex
   774   document_files "root.tex"
   775 
   776 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
   777   options [document = false]
   778   theories NSPrimes
   779 
   780 session "HOL-Mirabelle" in Mirabelle = HOL +
   781   options [document = false]
   782   theories Mirabelle_Test
   783 
   784 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   785   options [document = false, timeout = 60]
   786   theories Ex
   787 
   788 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
   789   options [document = false, quick_and_dirty]
   790   theories
   791     Boogie
   792     SMT_Examples
   793     SMT_Word_Examples
   794   theories [condition = ISABELLE_FULL_TEST]
   795     SMT_Tests
   796   files
   797     "Boogie_Dijkstra.certs2"
   798     "Boogie_Max.certs2"
   799     "SMT_Examples.certs2"
   800     "SMT_Word_Examples.certs2"
   801     "VCC_Max.certs2"
   802 
   803 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
   804   options [document = false]
   805   theories SPARK
   806 
   807 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   808   options [document = false]
   809   theories
   810     "Gcd/Greatest_Common_Divisor"
   811 
   812     "Liseq/Longest_Increasing_Subsequence"
   813 
   814     "RIPEMD-160/F"
   815     "RIPEMD-160/Hash"
   816     "RIPEMD-160/K_L"
   817     "RIPEMD-160/K_R"
   818     "RIPEMD-160/R_L"
   819     "RIPEMD-160/Round"
   820     "RIPEMD-160/R_R"
   821     "RIPEMD-160/S_L"
   822     "RIPEMD-160/S_R"
   823 
   824     "Sqrt/Sqrt"
   825   files
   826     "Gcd/greatest_common_divisor/g_c_d.fdl"
   827     "Gcd/greatest_common_divisor/g_c_d.rls"
   828     "Gcd/greatest_common_divisor/g_c_d.siv"
   829     "Liseq/liseq/liseq_length.fdl"
   830     "Liseq/liseq/liseq_length.rls"
   831     "Liseq/liseq/liseq_length.siv"
   832     "RIPEMD-160/rmd/f.fdl"
   833     "RIPEMD-160/rmd/f.rls"
   834     "RIPEMD-160/rmd/f.siv"
   835     "RIPEMD-160/rmd/hash.fdl"
   836     "RIPEMD-160/rmd/hash.rls"
   837     "RIPEMD-160/rmd/hash.siv"
   838     "RIPEMD-160/rmd/k_l.fdl"
   839     "RIPEMD-160/rmd/k_l.rls"
   840     "RIPEMD-160/rmd/k_l.siv"
   841     "RIPEMD-160/rmd/k_r.fdl"
   842     "RIPEMD-160/rmd/k_r.rls"
   843     "RIPEMD-160/rmd/k_r.siv"
   844     "RIPEMD-160/rmd/r_l.fdl"
   845     "RIPEMD-160/rmd/r_l.rls"
   846     "RIPEMD-160/rmd/r_l.siv"
   847     "RIPEMD-160/rmd/round.fdl"
   848     "RIPEMD-160/rmd/round.rls"
   849     "RIPEMD-160/rmd/round.siv"
   850     "RIPEMD-160/rmd/r_r.fdl"
   851     "RIPEMD-160/rmd/r_r.rls"
   852     "RIPEMD-160/rmd/r_r.siv"
   853     "RIPEMD-160/rmd/s_l.fdl"
   854     "RIPEMD-160/rmd/s_l.rls"
   855     "RIPEMD-160/rmd/s_l.siv"
   856     "RIPEMD-160/rmd/s_r.fdl"
   857     "RIPEMD-160/rmd/s_r.rls"
   858     "RIPEMD-160/rmd/s_r.siv"
   859 
   860 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   861   options [show_question_marks = false]
   862   theories
   863     Example_Verification
   864     VC_Principles
   865     Reference
   866     Complex_Types
   867   files
   868     "complex_types_app/initialize.fdl"
   869     "complex_types_app/initialize.rls"
   870     "complex_types_app/initialize.siv"
   871     "loop_invariant/proc1.fdl"
   872     "loop_invariant/proc1.rls"
   873     "loop_invariant/proc1.siv"
   874     "loop_invariant/proc2.fdl"
   875     "loop_invariant/proc2.rls"
   876     "loop_invariant/proc2.siv"
   877     "simple_greatest_common_divisor/g_c_d.fdl"
   878     "simple_greatest_common_divisor/g_c_d.rls"
   879     "simple_greatest_common_divisor/g_c_d.siv"
   880   document_files
   881     "complex_types.ads"
   882     "complex_types_app.adb"
   883     "complex_types_app.ads"
   884     "Gcd.adb"
   885     "Gcd.ads"
   886     "intro.tex"
   887     "loop_invariant.adb"
   888     "loop_invariant.ads"
   889     "root.bib"
   890     "root.tex"
   891     "Simple_Gcd.adb"
   892     "Simple_Gcd.ads"
   893 
   894 session "HOL-Mutabelle" in Mutabelle = HOL +
   895   options [document = false]
   896   theories MutabelleExtra
   897 
   898 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
   899   options [document = false]
   900   theories
   901     Quickcheck_Examples
   902     Quickcheck_Lattice_Examples
   903     Completeness
   904     Quickcheck_Interfaces
   905   theories [condition = ISABELLE_GHC]
   906     Hotel_Example
   907     Quickcheck_Narrowing_Examples
   908 
   909 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
   910   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
   911     Find_Unused_Assms_Examples
   912     Needham_Schroeder_No_Attacker_Example
   913     Needham_Schroeder_Guided_Attacker_Example
   914     Needham_Schroeder_Unguided_Attacker_Example
   915 
   916 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
   917   description {*
   918     Author:     Cezary Kaliszyk and Christian Urban
   919   *}
   920   options [document = false]
   921   theories
   922     DList
   923     FSet
   924     Quotient_Int
   925     Quotient_Message
   926     Lift_FSet
   927     Lift_Set
   928     Lift_Fun
   929     Quotient_Rat
   930     Lift_DList
   931     Int_Pow
   932 
   933 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   934   options [document = false]
   935   theories
   936     Examples
   937     Predicate_Compile_Tests
   938     (* FIXME
   939     Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
   940     Specialisation_Examples
   941     IMP_1
   942     IMP_2
   943     (* FIXME since 21-Jul-2011
   944     Hotel_Example_Small_Generator
   945     IMP_3
   946     IMP_4 *)
   947   theories [condition = "ISABELLE_SWIPL"]
   948     Code_Prolog_Examples
   949     Context_Free_Grammar_Example
   950     Hotel_Example_Prolog
   951     Lambda_Example
   952     List_Examples
   953   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]
   954     Reg_Exp_Example
   955 
   956 session HOLCF (main) in HOLCF = HOL +
   957   description {*
   958     Author:     Franz Regensburger
   959     Author:     Brian Huffman
   960 
   961     HOLCF -- a semantic extension of HOL by the LCF logic.
   962   *}
   963   options [document_graph]
   964   theories [document = false]
   965     "~~/src/HOL/Library/Nat_Bijection"
   966     "~~/src/HOL/Library/Countable"
   967   theories
   968     Plain_HOLCF
   969     Fixrec
   970     HOLCF
   971   document_files "root.tex"
   972 
   973 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   974   theories
   975     Domain_ex
   976     Fixrec_ex
   977     New_Domain
   978   document_files "root.tex"
   979 
   980 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   981   options [document = false]
   982   theories HOLCF_Library
   983 
   984 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   985   description {*
   986     IMP -- A WHILE-language and its Semantics.
   987 
   988     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   989   *}
   990   options [document = false]
   991   theories HoareEx
   992   document_files "root.tex"
   993 
   994 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
   995   description {*
   996     Miscellaneous examples for HOLCF.
   997   *}
   998   options [document = false]
   999   theories
  1000     Dnat
  1001     Dagstuhl
  1002     Focus_ex
  1003     Fix2
  1004     Hoare
  1005     Concurrency_Monad
  1006     Loop
  1007     Powerdomain_ex
  1008     Domain_Proofs
  1009     Letrec
  1010     Pattern_Match
  1011 
  1012 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
  1013   description {*
  1014     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
  1015 
  1016     For introductions to FOCUS, see
  1017 
  1018     "The Design of Distributed Systems - An Introduction to FOCUS"
  1019     http://www4.in.tum.de/publ/html.php?e=2
  1020 
  1021     "Specification and Refinement of a Buffer of Length One"
  1022     http://www4.in.tum.de/publ/html.php?e=15
  1023 
  1024     "Specification and Development of Interactive Systems: Focus on Streams,
  1025     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
  1026   *}
  1027   options [document = false]
  1028   theories
  1029     Fstreams
  1030     FOCUS
  1031     Buffer_adm
  1032 
  1033 session IOA in "HOLCF/IOA" = HOLCF +
  1034   description {*
  1035     Author:     Olaf Mueller
  1036     Copyright   1997 TU München
  1037 
  1038     A formalization of I/O automata in HOLCF.
  1039 
  1040     The distribution contains simulation relations, temporal logic, and an
  1041     abstraction theory. Everything is based upon a domain-theoretic model of
  1042     finite and infinite sequences.
  1043   *}
  1044   options [document = false]
  1045   theories "meta_theory/Abstraction"
  1046 
  1047 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
  1048   description {*
  1049     Author:     Olaf Mueller
  1050 
  1051     The Alternating Bit Protocol performed in I/O-Automata.
  1052   *}
  1053   options [document = false]
  1054   theories Correctness
  1055 
  1056 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
  1057   description {*
  1058     Author:     Tobias Nipkow & Konrad Slind
  1059 
  1060     A network transmission protocol, performed in the
  1061     I/O automata formalization by Olaf Mueller.
  1062   *}
  1063   options [document = false]
  1064   theories Correctness
  1065 
  1066 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
  1067   description {*
  1068     Author:     Olaf Mueller
  1069 
  1070     Memory storage case study.
  1071   *}
  1072   options [document = false]
  1073   theories Correctness
  1074 
  1075 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
  1076   description {*
  1077     Author:     Olaf Mueller
  1078   *}
  1079   options [document = false]
  1080   theories
  1081     TrivEx
  1082     TrivEx2
  1083 
  1084 session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
  1085   description {*
  1086     Some rather large datatype examples (from John Harrison).
  1087   *}
  1088   options [document = false]
  1089   theories [condition = ISABELLE_FULL_TEST, timing]
  1090     Brackin
  1091     Instructions
  1092     SML
  1093     Verilog
  1094 
  1095 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
  1096   description {*
  1097     Some benchmark on large record.
  1098   *}
  1099   options [document = false]
  1100   theories [condition = ISABELLE_FULL_TEST, timing]
  1101     Record_Benchmark
  1102