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