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