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